[Haskell-cafe] Type without a data constructor?

[Robert Dockins]

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