АК
та не
Size: a a a
2021 October 24
И
то вылезут эти самые ошибки
АК
вроде красным подсвечивает
И
хм, сейчас еще раз посмотрю, но он пишет мне что Pattern match(es) are non-exhaustive
И
а с Minus типо получше вариант?
И
или есть еще какие то способы сделать что-то подобное?
АК
лучший вариант - это тот, где у меня хлс для этого метода анекзостив матч не подсвечивает
АК
а как он должен выглядеть - хз
АК
это лучше спросите в основном чате, там больше людей умеющих жонглировать на тайплевеле, чем в чате для новичков
И
Ок, спасибо. С Minus вроде такого нет. А вот твой вроде и подсвечивает non-exhaustive, но на каких то базовых примерах работает.
И
я кстати твой вариант вроде починил, там надо было в тайп фемили добавить еще 1 паттерн -
LessThan a 'Zero = ('False ~ 'True)2021 October 25
АК
та это, вроде, не важно - оно в обоих случаях в компайл тайме упадет
АК
лучший вариант - это скорее всего сделать с
Fin n, как во всяких туториалах по языкам с зависимыми типамиАК
что-то вроде
data Fin (n :: Nat) where
FZ :: Fin n
FS :: Fin n -> Fin ('Succ n)
getAt3 :: Vector a ('Succ n) -> Fin n -> a
getAt3 (x :| _) FZ = x
getAt3 (x :| xs) (FS m) = getAt3 xs m
main = do
print $ getAt3 (1 :| 2 :| 3 :| Nil) (FS $ FS FZ)
И
этот
Fin вроде полный аналог SNat из задачи.И
просто имя другое
И
Если честно, я в этой теме почти ничего не понимаю. В твоем решении если в LessThan передать первым аргментом "число" большее чем вторым аргументом, то получится нечто странное
:k! LessThan ('Succ ('Succ ('Succ 'Zero))) ('Succ ('Succ 'Zero))
LessThan ('Succ ('Succ ('Succ 'Zero))) ('Succ ('Succ 'Zero)) :: Constraint
= LessThan ('Succ 'Zero) 'Zero
И как конкретно компилятор обработает вот этот констрейнт`LessThan ('Succ 'Zero) 'Zero` я даже не представляю.И
а если добавить тот самый паттерн что я скинул, то получится такое:
:k! LessThan ('Succ ('Succ ('Succ 'Zero))) ('Succ ('Succ 'Zero))
LessThan ('Succ ('Succ ('Succ 'Zero))) ('Succ ('Succ 'Zero)) :: Constraint
= ('False ~ 'False, ('True ~ 'False, ('False ~ 'False, () :: Constraint)))
а это ('False ~ 'False, ('True ~ 'False, ('False ~ 'False, () :: Constraint))) уже вроде нормальный констрейнт получаетсяАК
> И как конкретно компилятор обработает вот этот констрейнт`LessThan ('Succ 'Zero) 'Zero` я даже не представляю.
Никак - просто ошибку кинет, если нужно что-бы был красивый констрент и внятное сообщение об ошибке есть https://hackage.haskell.org/package/base-4.15.0.0/docs/GHC-TypeLits.html#t:TypeError
Никак - просто ошибку кинет, если нужно что-бы был красивый констрент и внятное сообщение об ошибке есть https://hackage.haskell.org/package/base-4.15.0.0/docs/GHC-TypeLits.html#t:TypeError