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

[Claus Reinke]

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

> 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]

>assuming that:
>- 'module X[types]' means a module parameterized by 'types'
>- 'import X[types]' means a module import with parameters 'types'.

It appears I need to qualify my earlier statement that Haskell doesn't
have parameterized modules and type sharing (thanks to Tuve Nordius
[1] for suggesting to use type families for the former). Here is an encoding 
of the hypothetical example above using type families (using one of their 
lesser publicized features - they can be referred to before being defined):

----------------------------------------------------
{-# LANGUAGE TypeFamilies #-}
module LA where 

type family Label a
z = undefined::Label ()

----------------------------------------------------
{-# LANGUAGE TypeFamilies #-}
module LB where 

type family Label a
z = undefined::Label ()

----------------------------------------------------
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
module LC where
import LA
import LB

-- express type sharing while leaving actual type open
type family Label a
type instance LA.Label a = LC.Label a
type instance LB.Label a = LC.Label a
ok2 = [LA.z,LB.z]
----------------------------------------------------

Modules 'LA' and 'LB' use the applications of the yet to be instantiated
type family 'Label a' as placeholders for unknown types (ie, type families
are used as glorified type synonyms, but with delayed definitions), effectively 
parameterizing the whole modules over these types. Module 'LC' adds
its own placeholder 'LC.Label a', instantiating both 'LA.Label a' and
'LB.Label a' to the same, as yet unknown type (we're refining their
definitions just enough to allow them to match identically), effectively 
expressing a type sharing constraint.

This is probably implicit in the work comparing SML's module language
with Haskell's recent type class/family extensions (can anyone confirm
this with a quote/reference?), but I hadn't realized that this part of the
encoding is straightforward enough to use in practice.

One remaining issue is whether this encoding can be modified to allow
for multiple independent instantiations of 'LA', 'LB', and 'LC' above,
each with their own type parameters, in the same program.

Claus

[1] http://www.haskell.org/pipermail/haskell-cafe/2009-April/060665.html