• ? :( Haskell typefun type family LessThen255 n :: Constraint where
    LessThen255 f = (f <= 255)

    class KnownNat n => FindEq (c::Nat -> Constraint) (n::Nat) where
    findEq :: (KnownNat p) => Proxy n -> Proxy p -> Maybe (Proof2 c)

    instance FindEq LessThen255 0 where findEq = Nothing
    а так, что нельзя чтоли?

Replies (7)

  • @qnikst, Наты уже можно вовсю использовать?
  • @fmap, Использовать можно — вовсю точно нет, тайпчеккер тупит иногда (во времени и ограничениям на глубину и кол-во контекстов) и некоторые вещи типа рекурсии неудобно делать. Вроде обещали сделать конвертилку в числа Чёрча (ну которые S N | Z) тогда по приятнее будет между представлениями прыгать.
  • @qnikst, почему не писать вещи, требующие верификации, на Agda и не линковать выхлоп MAlonzo с хаскельным кодом?
  • @jtootf, Потому что интерес исключительно в том, чтобы понять что можно писать на хацкеле не лазая в более сильные инструменты :)
  • @qnikst, рационально, но нездраво :)
  • @jtootf, А вообще я не умею в агду, т.к. не было задач где оно действительно надо :(
  • @qnikst, Agda намного проще Haskell и полезна для общего развития независимо от наличия задач. но евангелировать не буду