...

- 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;-)

Tillmann Rendel wrote:

Hi Claus,

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.

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.

...

Standard ML's answer to that kind of issue is type sharing.

Does type sharing help with making modules retroactively compatible?

map (\i -> rot13 i) import Foo -- (c) this sig last receiving data processing entity. Inspect headers for copyright history. All rights reserved. Copying, hiring, renting, performance and/or quoting of this signature prohibited.

in case anyone stumbles over my ad-hoc notations, that should have been:

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'. Claus

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

z :: client -> Label client z client = undefined

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

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.

In particular, this variant requires all bindings in the module to take an explicit parameter, instead of having a single parameter for the whole module. Having a single module-identifier parameter for each binding is better than having lots of individual parameters for each binding, but the idea of a parameterized module is to avoid these extra per-binding parameters alltogether. Of course, my variant cheated a little, using the TF "feature" that TF applications hide implicit parameters from contexts, so instead of 'Label a~type=>type', we write 'Label a'. (which meant I had to fix the 'a' to something concrete to avoid ambiguous types, as I needed to use type families, not data families, to get the sharing) Nevertheless, interesting possibilities. Claus