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

[Claus Reinke]

>> - 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')
> 
> How is the need for a common import for 'data TTrue; data TFalse' 
> different then the need for a common import for 'data Bool = True | False'?

'Bool' is hardcoded at the language level (if/then/else), not just standard
library, not just implicitly imported Prelude, so that seems very stable - 
stable enough for a single common standard library import (unlike many
type-level programming concepts, which still require experimentation
and variation).

But even that is considered too unflexible - some users want alternative
Preludes (be it temporarily, to develop a better standard, or permanently,
for personal preferences), most authors of embedded domain-specific 
languages have wanted to replace 'Bool' and associated syntax/classes/
operations with a variant matching their needs.

Now you have several definitions of 'Bool', some of which may be
compatible with each other (say, two variants of FRP libraries that
both simply lift 'Bool' into 'Time->Bool'). How do you, as a library 
user, express that two compatible types from different sources are 
to be considered equivalent, without forcing the authors of the 
compatible definitions to collaborate on a common "standard" 
library for both their projects? It is not a question of possible-in-theory,
it is a question of pragmatics.

The need to go beyond common imports, temporarily (as systems
evolve) or permanently (because tree-like hierarchies do not fit
all modularization strategies), exists for 'Bool' as well as for 'TBool'.

Standard ML's answer to that kind of issue is type sharing. Haskell 
has no equivalent. Haskell has further needs in going beyond plain
hierarchical import structures, though - think of the proposals for 
class aliases, or the question of how to split up package dependencies 
without relying on orphan instances, how to depend on packages in 
specific configurations, etc. Again, the ML family of advanced module
systems has some answers to offer (and, yes, we can encode much
of those in Haskell's type system, but who does that when writing
cabal packages?).

Haskell'98, by design, had the simplest module system it could get
away with. These days, additional layers have accumulated around
this core, based on libraries and cabal packages. These layers run
into all the problems of advanced module systems, only that these
problems currently  aren't acknowledged as language design 
problems, but are treated as issues to hack around whenever 
someone is available to do the hacking.

> Clearly, the advent of type-level programming necessitates the design of 
> a type-level standard library, which provides standard abstractions to 
> enable interoperation of custom libraries. But I don't see why the 
> module system should not scale to type-level programming.

Haskell's module system is an embarrassment ignoring decades
of research, its one strong point being its simplicity. There has long
been an implicit assumption that advances in modular programming
would come either via the type class system, or via extensible records,
and that these advanced would happen within modules, without having
to evolve the module system beyond simple namespace management.

In practice, cabal and hackage have changed all that, introducing a
de-facto module configuration system on top of the existing modules, 
with an evolving design.

My typed non-atomic atoms don't fix any of that, but they do seem
to offer a workaround for a single issue that has been around for years,
and has led to several trac tickets and type-level library awkwardnesses.
For instance, it isn't necessary to pre-define hundreds of constant literals 
for a type-level numeric library if they can be generated in client code,
nor is it necessary to hand-define or template-generate an ordering
relation on constructors (which some type-level libraries depend on)
if it can be defined once and for all.

Non of this means that it wouldn't be good to have a standard
library for type-level programming - in fact, I'd expect a revised 
Data.Label to become a small part of such standard!-)

Claus

ps. If you want to know more about my view on module systems
    for functional languages, have a look at chapter 4 of
    http://community.haskell.org/~claus/publications/phd.html ,
    titled "Module Systems for Functional Languages". 

    It is slightly dated by now -lots of things have happened in program 
    (de-)composition research since 1997, when that was written-, but 
    the basis for Haskell's module system is much more ancient that that, 
    so it might be interesting for new Haskellers to see just how old
    some of Haskell's "advanced" ideas really are;-)