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

[Tillmann Rendel]

Hi,

Claus Reinke wrote:
> 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.

Modules A and B can make their dependence on the ultimate client module 
more explicit.

   {-# LANGUAGE TypeFamilies #-}
   module A where
     type family Label client
     z :: client -> Label client
     z client = undefined

   {-# LANGUAGE TypeFamilies #-}
   module B where
     type family Label client
     z :: client -> Label client
     z client = undefined

A client of A and B can just use them together, and ghc figures out the 
sharing constraints.

   {-# LANGUAGE TypeFamilies #-}
   module C where
     import A
     import B

     ok client = [ A.z client, B.z client]

The type inferred for C.ok is

   ok :: (B.Label client ~ A.Label client) =>
         client -> [A.Label client].

This seems to be already quite useful. However, a different client of A 
and B could hide it's use of A and B, and the type sharing constraints, 
from its own clients.

   {-# LANGUAGE TypeFamilies #-}
   module D (ok) where
     import A
     import B

     data D client = D client

     type family Label client
     type instance A.Label (D client) = D.Label client
     type instance B.Label (D client) = D.Label client

     ok :: client -> [D.Label client]
     ok client = [ A.z (D client), B.z (D client)]

Note that D does not export the reified module identity D, and that the 
type of D.ok does not expose the fact that D is implemented in terms of 
A and B.

This technique relies on the explicit management of the identities of 
modules both at compile-time (type annotation of D.ok) and run-time 
(creation of (D client) in the body of D.ok). While explicit management 
of modules at compile time is the point of the exercise, it would be 
better to avoid the passing of reified module identities at runtime.

   Tillmann