Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

Tags:

haskell

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.

like image 768
aqui8 Avatar asked Sep 10 '20 23:09

aqui8


People also ask

What is a triple colon?

tricolon (plural tricolons or tricola) (rhetoric) A sentence with three clearly defined parts of equal length, usually independent clauses.

What Does a colon mean in Haskell?

In Haskell, the colon operator is used to create lists (we'll talk more about this soon). This right-hand side says that the value of makeList is the element 1 stuck on to the beginning of the value of makeList .

What is $! In Haskell?

$! is strict application, the difference from dispatch state1 is that state1 is guaranteed to be evaluated and not just kept as a lazy thunk. It's defined as f $! x = x `seq` f x. Forcing evaluation in this way can be important for efficiency issues, such as preventing memory leaks.

What is cons in Haskell?

Cons is a historic name, though, originating from Lisp. :-: is another arbitrary name for the constructor, except that it can be used infix. I.e. instead of Cons 1 someList one can write 1 :-: someList .


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    →  .. | : | :: | = | \ | | | <- | -> |  @ | ~ | =>
like image 148
Willem Van Onsem Avatar answered Oct 12 '22 19:10

Willem Van Onsem


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
like image 3
Iceland_jack Avatar answered Oct 12 '22 20:10

Iceland_jack