[Haskell-cafe] Non-atomic "atoms" for type-level programming

[Claus Reinke]

> thanks for your elaborations. I'm still not convinced that a common name 
> (e.g. TT :. Tr :. Tu :. Te) is a better interface than a common import 
> (e.g. TypeLevel.Bool.True). In both cases, the authors of all modules 
> have to actively collaborate, either to define common names, or to 
> define common imports.

It is not a solution, it is a workaround. All it does is offer users another 
choice, so they can now say whether they are talking about shared or
locally defined labels:

module A where 
import Data.Label
data MyLabel
x = [$l|label|]
y = undefined::MyLabel

module B where 
import Data.Label
data MyLabel
x = [$l|label|]
y = undefined::MyLabel

module C where
import Data.Label
import A
import B
ok = [A.x,B.x]
fails = [A.y,B.y]

It does so by offering a meta-level commonality: A and B do not have
to agree on a common module to declare all their common types (the 
author of Data.Label has no idea what labels its importers might use,
other than the alphabet the labels are constructed from), they only 
need to agree on a common way of declaring all their shareable types.

> But I begin to see how type-level atoms could help to, e.g., implement 
> more advanced module system as type-level embedded DSLs in Haskell.

Well, atoms make labels, labels form extensible record fields, extensible 
records can be used as first-class modules, but there'd still be a lot missing.

This is really just a small step, and though it is a useful one, it has no such
high aspirations, yet. When I wrote the first-class-labels proposal for
Haskell', I was thinking about possible implementations (outlined in the
haskell prime wiki page I referred to) but they always looked as if they'd
require substantial changes. This workaround suggests that a few 
well-placed localised changes to GHC might be sufficient to get first-class
labels - just split the modifications over two, only losely coupled areas:

- provide label constructors
- provide label usage (preferably hiding the internal structure)

Until someone does that, quasiquoting offers a workaround, so people
can resume playing with things like type-level numbers, extensible record
libraries with and without label ordering, etc. I've filed a feature request
for type-level quasiquoting, in case anyone else has such needs:-)

http://hackage.haskell.org/trac/ghc/ticket/3177

>> Standard ML's answer to that kind of issue is type sharing.
> 
> Does type sharing help with making modules retroactively compatible?

It has been too long since I looked at this in detail, but yes. The way
I recall it (and the early example in [1] seems to confirm this, though
SML has changed after that paper was published) is that modules
have signatures, and type sharing constraints assert that parts of
these signatures have to match up (in Haskell-speak: imagine modules
as records, with two records R1 a and R2 b, then we can use a type 
'a~b => R1 a -> R2 b -> T' to assert that both records share the
same type parameter; only that Haskell modules aren't records
and aren't parameterized..).

It would be as if one could write modules parameterised by types,
instead of declaring them locally, and being able to share a type
parameter over several imports:

module A(type label) where x = undefined :: label
module B(type label) where x = undefined :: label

module C(type label) where
import A[label]
import B[label]
ok = [A.x,B.x]

Claus

[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.14.3595
    Robert Harper and Mark Lillibridge,
    A Type-Theoretic Approach to Higher-Order Modules with Sharing