Re: [Haskell-cafe] singleton types

lrpalmer:

2010/4/25 Günther Schmidt :

...

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