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

[Claus Reinke]

The recent GHC trac ticket revision reminded me of the old open
type-sharing problem with type tags and record labels:

- if type-level tags (such as 'data TTrue'/'data TFalse') are declared
    repeatedly in separate modules, they represent separate types,
    preventing shared use (your type-level predicate doesn't return
    my version of 'TTrue'/'TFalse')

- if record field labels (as used in your run-of-the-mill extensible
    record library) have to be declared, that is not only inconvenient,
    but prevents sharing of field labels over independent code bases

    (see the old Haskell' ticket #92 for discussion
    http://hackage.haskell.org/trac/haskell-prime/wiki/FirstClassLabels ;
    also http://hackage.haskell.org/trac/ghc/ticket/1872 for alternative
    extensible records libs)

Since Haskell has no concept of type sharing, the only way to express
this is to declare types in a common import. But there is no way for
that common import to predict all possible future uses, and we can't
just keep adding more labels/tags to it, forcing all dependencies to
be updated and kept in sync.

Using Template Haskell, and QuasiQuotes in particular, we can now
at least work around this issue, by splitting the atoms:-)

- 'undefined :: Tag' becomes 'undefined :: (TT :. Ta :. Tg)'

- 'label :: Label' becomes '(Ll :< La :< Lb :< Le :< Ll) :: (Ll :< La :< Lb :< Le :< Ll)'

- a common import, Data.Label, provides type letters and combinators:

    'data La = La' and 'data a :< b = a :< b'
    'data Ta' and 'data a :. b'   
    ..

- quasiquoting and Show instances, also provided by Data.Label, try to 
    hide the internal structure of labels and tags, at least at expression level. 
    Since there is no quasiquoting at type-level (why?), generating type 
    synonyms seems the best we can do there..

- since record field labels are constructed from type letters, this would
    also provide a basis for
    - type-level numbers (type-level quasiquoting would help, though)
    - label ordering:
        http://hackage.haskell.org/trac/ghc/ticket/2104
        http://hackage.haskell.org/trac/ghc/ticket/1894

In actual use, this is what tags and labels from Data.Label look like:

-------------
-- the usual extensible-records-as-nested-pairs
data label := value  = label := value  deriving Show
data field :& record = field :& record deriving Show
infixr :&

-- no quasiquoting for types:-(, so generate type synonyms instead
$(genTypeTag "TTrue")
$(genTypeTag "TFalse")

-- a type-level predicate, using shared tags TTrue/TFalse
class HasField record label tbool | label record -> tbool
instance HasField ()                       label TFalse
instance HasField ((label:=value):&record) label TTrue
instance HasField record                   label tbool 
      => HasField (field:&record)          label tbool

-- record field selection, driven by field label types
class Select record label value where (!) :: record -> label -> value
instance ..

-- some example records 

-- no need to declare field labels, and they will be
-- shared with other importers of Data.Label!
a = ([$l|this|] := True)
  :&([$l|that|] := "hi")
  :&()

b = ([$l|that|] := "there")
  :&([$l|x|] := 100)
  :&([$l|y|] := 200)
  :&()

-- we don't even need label values for this, 
-- type tags are sufficient, as long as we don't
-- evaluate the (undefined) values of tags
c = ([$t|this|] := 'x')
  :&([$t|y|] := ())
  :&()

-- testing Show and record selection
records = do
  print a
  print b
  print c
  print $ (a ! [$l|this|])
  print $ (c ! [$t|this|])
  print $ (a ! [$l|that|]) ++ ", " ++ (b ! [$l|that|])

-------------
*Main> [$l|label|]
label
*Main> :t [$l|label|]
[$l|label|] :: Ll :< (La :< (Lb :< (Le :< Ll)))
*Main> [$l|label|] `seq` ()
()
*Main> [$t|label|]
label
*Main> :t [$t|label|]
[$t|label|] :: Tl :. (Ta :. (Tb :. (Te :. Tl)))
*Main> [$t|label|] `seq` ()
*** Exception: Prelude.undefined

*Main> :t [$l|100|]
[$l|100|] :: L1 :< (L0 :< L0)

*Main> records
(this := True) :& ((that := "hi") :& ())
(that := "there") :& ((x := 100) :& ((y := 200) :& ()))
(this := 'x') :& ((y := ()) :& ())
True
'x'
"hi, there"
-------------

For example code, see 
    http://community.haskell.org/~claus/misc/Data/Label.hs
    http://community.haskell.org/~claus/misc/Data/Label/TH.hs
    http://community.haskell.org/~claus/misc/labels.hs

Claus