[Haskell-cafe] singleton types

[Don Stewart]

lrpalmer:
> 2010/4/25 Günther Schmidt <gue.schmidt at web.de>:
> > Hello,
> >
> > HaskellDB makes extensive use of Singleton Types, both in its original
> > version and the more recent one where it's using HList instead of the legacy
> > implementation.
> >
> > I wonder if it is possible, not considering feasibility for the moment, to
> > implement HaskellDB *without* using Singleton Types.
> 
> Would you please define "singleton type"?

Funny, we had a discussion about this at work this week (in the context
of adding singleton types to Cryptol to support some witness/proof
work).

A nice defn is Oleg's:

    http://okmij.org/ftp/Computation/lightweight-dependent-typing.html#Singleton

    "we define particular types such that the corresponding sets of values
    consist of only one value, the conceptual barrier between elements and
    sets of elements disappears"

Which is the intuitive notion, I think.

-- Don