On Monday 06 August 2007 19:23, Rahul Kapoor wrote:
Most examples for defining algebraic types include data constructors like so:
data Tree a = Tip | Node a (Tree a) (Tree a)
I by mistake defined a type which did not specify a data constructor :
In this example, you have two different uses of the lexical name 'Term', and I think it is confusing you. One kind of use is as a data constructor; the other is as a type constructor. I've annotated the uses below:
data SearchCondition = Term Bool -- data constructor | SearchCondition :||: (Term Bool) -- type constructor
data Term a = Constant a -- defn of type constr 'Term'
sc :: SearchCondition sc = Term True -- data constructor
is ok, but
sc :: SearchCondition sc = Constant True
Now, here you have an expression of type 'Term Bool'. These can only appear on the right-hand side of :||: . This probably isn't what you want. Likely what you actually want is:
data SearchCondition = SearchTerm (Term Bool) | SearchCondition :||: (Term Bool)
Here, both uses of 'Term' refer to the type constructor.
is not (though this is what I intended to capture!).
So the question is what are types with no constructors good for? A simple example would be appreciated.
There are some situations where an explicitly empty type is useful. Type-level programming voodoo is one. Other times the void type is nice because it can be used as a parameter to a type constructor. For example, if you use the nested datatype representation of de Bruijn lambda terms [1], you can use the void type to create the type of closed terms (terms with no free variables). Here's the short version: data Void data Succ a = Zero | Incr a data Term a = Var a | App (Term a) (Term a) | Lam (Term (Succ a)) type ClosedTerm = Term Void [1] Richard Bird and Ross Patterson, _de Brujin Notation as a Nested Datatype_, Journal of Functional Programming 9(1):77-91, January 1999. Rob Dockins