Nat) a
= n ~ Z => VNil n a
| forall m. n ~ S m => VCons a (Vec m a)
Expected a type, but ‘n’ has kind ‘Nat’
как такое решить?
Взять Idris?)
я конечно ждал такого ответа, и идрис или даже gadts в хаскель это решит, но мой вопрос был именно в пределах обычного адт
покажи VNil
он там же
запись VNil n a означает конструктор VNil с 2 полями данных. первое данное имеет тип n. но ты же не сможешь подсунуть сюда данное типа n
это будет семантически гадт, но в синтаксисте обычного адт
ты же какую-то чушь написал {-# LANGUAGE KindSignatures, DataKinds, GADTs #-} data Nat = Z | S Nat data Vec n a = n ~ Z => VNil | forall m. n ~ S m => VCons a (Vec m a)
знаю) я уже написал причину, спать надо больше
А в чем преимущества Haskell перед другими языками/технологиями? Например, читаешь такой код, и думаешь - как такое можно понять? И чем это лучше кода на других языка? Просто интересно
Например, читаешь такой код, и думаешь - как такое можно понять? Потом прочитал любое введение — и понял.
преимущества в сопровождаемости. даже если вообще не знаешь, как устроена программа, можно править код, а компилятор сообщит, где возникают противоречия
data Vec len a where Nil :: Vec 0 a Cons :: a -> Vec len a -> Vec (len + 1) a Так лучше?
чуть лучше) я так понимаю, тут создается вектор Vec с длиной a? или в len подставляется длина, а в a подставляется элемент?
len - длина, a - тип элемента
а куда кладется сам элемент?
Но это наивная реализация. Не-наиваной будет вектор с type-indexed обёрткой.
Cons :: a -> Vec len a -> Vec (len + 1) a первый аргумент конструктора - a, это и есть элемент второй аргумент - хвост Cons :: a -> Vec len a -> Vec (len + 1) a а на выходе будет значение типа Cons :: a -> Vec len a -> Vec (len + 1) a
Первый параметр у конструктора Cons
Cons 1 (Cons 2 (Cons 3 Nil)) :: Vec 3 Int
сначала прочийте любое введение в Хаскель, например, http://learnyouahaskell.com, чтобы понимать основы
Обсуждают сегодня