Can someone explain this function and how to type it in Haskell (infix, :-:)

user_17636851 0
Viewed 81
infixr 5 :-:  
data List a = Empty | a :-: (List a) deriving (Show, Read, Eq, Ord)

we just wrote a :-: (List a) instead of Cons a (List a). Now, we can write out lists in our list type like so:

ghci> 3 :-: 4 :-: 5 :-: Empty  
(:-:) 3 ((:-:) 4 ((:-:) 5 Empty))  
ghci> let a = 3 :-: 4 :-: 5 :-: Empty  
ghci> 100 :-: a  
(:-:) 100 ((:-:) 3 ((:-:) 4 ((:-:) 5 Empty)))

I get that :-: is supposed to work like Cons but I don't really get why we are allowed to do that and how to actually type infixr 5 :-: .

infix-notation haskell types
1 Answers

I get that :-: is supposed to work like Cons but I don't really get why we are allowed to do that …

Because the Haskell report says so. In the grammar the constr is a data constructor. The constr can be a con followed by zero, one or more types, a con followed by record syntax, or a type, an operator conop followed by another type. This is defined as:

constr  →  con [!] atype1 … [!] atypek
        |  (btype | ! atype) conop (btype | ! atype)
        |  con { fielddecl1 , … , fielddecln }

The conop can be an operator consym, or an infix variant of an identifier between backticks, like `foo`, which is written in the grammar section as:

conop    →  consym | ` conid `

The grammar specifies that a consym is defined as:

consym → ( : {symbol })〈reservedop〉

so a colon followed by a sequence of symbols and such symbol should not be a reserved operator like :, ::, etc.

This thus means that except for the reserved operators, you can use operators that start with a colon (:) as a data constructor.

… and how to actually type infixr 5 :-:.

You can write multiline statements by surrounding these with :{ and :}:

ghci> :{
| infixr 5 :-:  
| data List a = Empty | a :-: (List a) deriving (Show, Read, Eq, Ord)
| :}
user_675790
Related