AP
Всякие очереди тоже обычно только в контексте IO можно читать и изменять
Size: a a a
2021 October 23
AP
Вот код, который с вынутыми из очереди элементами работает, может быть чистым — до момента записи, где опять потребуется выйти в мир IO
v
Понял, спасибо большое)
2021 October 24
YP
Бэнги в
!foo <- …
и
where
!bar = …
имеют смысл?
!foo <- …
и
where
!bar = …
имеют смысл?
[
вернее, смотря, как ты их используешь, конечно, но в целом да
И
Всем привет, а существет что то обратное type equality (
~)? Есть ли возможность констрейнтом указать что 2 типа не эквивалентны?JS
попробуйте
(a == b) ~ FalseИ
да, спасибо, я уже нагуглил
И
Хотел бы попрость вас помочь мне разобраться в ошибках, но не решать за меня задачу :)
Пытаюсь решить вот это https://ulearn.me/course/fpintroduction/getAt_dlya_Vector_review__06e06b36-5db6-44d9-8110-e15d4128fa84
Задача реализовать функцию
и индекс (тоже по сути реализованные через
Первые две мысли, которые пришли мне в голову - это либо создание тайп фэмили функции
Вторая идея - это создание тайп фэмили функции
Вот тут есть оба варианта - https://replit.com/@GracefulPotato/SpiritedEffectiveInstitute#main.hs, там можно убрать комментарии с 1 варианта, накинуть на 2 и посмотерть на другую ошибку.
Пытаюсь решить вот это https://ulearn.me/course/fpintroduction/getAt_dlya_Vector_review__06e06b36-5db6-44d9-8110-e15d4128fa84
Задача реализовать функцию
getAt, которая принимает вектор фиксированный длины (реализованные через Nat)и индекс (тоже по сути реализованные через
Nat). И надо сделать, что бы все ошибки, связанные с выходом за границы вектора были во время компиляции.Первые две мысли, которые пришли мне в голову - это либо создание тайп фэмили функции
LessThan, которая берет 2 Nat типа, и создает Constraint, рекурсивно проверяя, что первый тип не равен второму и что уменьшенный на единицу первый тип не равен второму.Вторая идея - это создание тайп фэмили функции
Minus, которая вычитает из первого Nat типа второй и в самой функции сделать констрейнт (Minus m n ~ 'Zero) =>
Ни первый ни второй вариант завести не могу, натыкаюсь на разные ошибки, которые расшифровать у не получается.Вот тут есть оба варианта - https://replit.com/@GracefulPotato/SpiritedEffectiveInstitute#main.hs, там можно убрать комментарии с 1 варианта, накинуть на 2 и посмотерть на другую ошибку.
И
А, всё, я походу решил, я паттерн матчил вектор так, что в
xs мог оказаться пустой вектор, а в типе стояло ограничение что вектор должен иметь такой тип - Vector a ('Succ n)И
вот так все заработало -
getAt (x :| y :| xs) (SSucc m) = getAt (y :| xs) m для варианта с MinusИ
А вот с LessThan чего то не выходит у меня.
АК
type family LessThan (x :: Nat) (y :: Nat) :: Constraint where
LessThan 'Zero 'Zero = 'False ~ 'True
LessThan 'Zero b = ()
LessThan ('Succ a) ('Succ b) = LessThan a b
getAt2 :: (LessThan m n) => Vector a n -> SNat m -> a
getAt2 (x :| _) SZero = x
getAt2 (x :| xs) (SSucc m) = getAt2 xs m
main = do
print $ getAt2 (1 :| 2 :| 3 :| Nil) (SSucc $ SSucc SZero)
АК
можно вот так сделать, но, наврное, так делать не нужно
И
а вот тут не все на этапе компиляции чекается
И
можно вызвать getAt на пустом векторе
И
и не получить ошибку компиляции
И
при этом если поправить сигнатуру у функции и сделать
Vector a ('Succ n)