Блог

Что означает тройное двоеточие (:::) в типе данных в Haskell?

Например: data Term = Var ID | Atom String | Nil | Term:::Term

Который находится в этой статьеhttps://gup.ub.gu.se/file/207634

Как бы это использовалось?

Например, я могу сделать, foo = Var "hello" но я не знаю, какая польза Term:::Term была бы.

(:::) это имя конструктора данных. Таким образом, вы можете определить Term тип с помощью:

 data Term = Var ID | Atom String | Nil | (:::) Term Term  

итак, точно так же, как у вас есть Var , Atom и Nil в качестве конструкторов данных, (:::) также является конструктором данных. Этот конструктор данных принимает два параметра, которые оба имеют Term типы. Например, список имеет (:) в качестве конструктора данных.

Конструкторы данных могут представлять собой последовательность символов, если они начинаются с двоеточия ( : ), и если это не зарезервированный оператор, такой как : , :: и т.д. Это указано в синтаксической ссылке отчета Haskell:

 consym        →   ( : {symbol})⟨reservedop⟩
reservedop    →  .. | : | :: | = |  | | | <- | -> |  @ | ~ | =>  

Было бы понятнее с синтаксисом GADT?

 data Term :: Type where
  Var   :: ID -> Term
  Atom  :: String -> Term
  Nil   :: Term
  (:::) :: Term -> Term -> Term
  

Эти подписи соответствуют выводам :kind и :type :

 >> :k Term
Term :: *
>> :t Var
Var :: ID -> Term
>> :t Atom
Atom :: String -> Term
>> :t Nil
Nil :: Term
>> :t (:::)
(:::) :: Term -> Term -> Term