What does triple colon (:::) in a data type mean in haskell?

user_2017673 0
Viewed 456

What does triple colon (:::) in a data type mean in Haskell?

For example: data Term = Var ID | Atom String | Nil | Term:::Term

Which is found in this paper https://gup.ub.gu.se/file/207634

How would it be used?

For example, I can do foo = Var "hello" but I don't know what use Term:::Term would be.

haskell
2 Answers

(:::) is the name of the data constructor. You can thus define the Term type with:

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

so just like you have Var, Atom, and Nil as data constructors, (:::) is a data constructor as well. This data constructor takes two parameters which both have Term types. A list has (:) as data constructor for example.

Data constructors can be a sequence of symbols, given these start with a colon (:), and given it is not a reserved operator like :, ::, etc. This is specified in the Syntax reference of the Haskell report:

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

Would it be clearer with GADT syntax?

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

These signatures match the output of :kind and :type:

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