Myself and Lucilia ([EMAIL PROTECTED]) have modified Mark Jones'
program, "Typing Haskell in Haskell",
(http://www.cse.ogi.edu/~mpj/thih) to support system CT (paper
available at http://www.dcc.ufmg.br/~camarao/ct.ps.gz). (Thanks Mark.)
The implementation is a prototype of system CT, mainly an adaptation
of system CT to deal with (possibly mutual) recursion in binding
groups. The source code is available at
http://www.dcc.ufmg.br/CT/CTinH.tar.gz . We would be very pleased to
receive comments, suggestions etc.
-- Overview of System CT
System CT extends ML-like type inference for supporting
overloading, with no special constructs for coping with
overloading. Types are inferred, with no mandatory type annotations
and no restrictions.
-- Abstract data are abstract
No conflict arises then between data abstraction and types of
overloaded symbols: constraints on types of terms (using
overloaded symbols or not) are automatically inferred. Types must
not be "determined" a priori by programmers, according to which
overloading symbols are used (an implementation-dependent issue).
In Haskell:
_________________________________________
| class Collection c where |
| ... |
| member:: Eq a => a -> Set a -> Bool |
| ... |
| instance Collection Set where |
| ... |
| member ... |
| ... |
|_______________________________________|
In CT:
______________
| ... | - No class and instance declarations required
| member ... | - No constraints required in type annotations
| ... | - No mandatory type annotation
|____________| - More importantly:
No obligation to a priori "determine" (and specify) the types and
constraints of classes and their members (there are many possible
ways of implementing collections)
-- Generality
Support of overloading of constants and functions, including
functions defined over different type constructors, with no
restriction on the syntactic form and number of parameters of
types. No monomorphism restriction.
For example, using (predefined map on lists and) map on trees
enabled by:
______________________________________________
| map f Leaf = Leaf |
| map f (Node a b) = Node (map f a) map f b) |
|____________________________________________|
Overloading is possible in any let binding, and even inside lambda
abstractions. This does not mean that these should be supported in a
language, but difficulties introduced by overloading in expressions
such as in the following example have been studied:
(let o = ...
o = ... in e) (let o = ...
o = ... in e')
-- Simple and informative types
Overloading in a closed world means that types are inferred
according to visible definitions. This enables the inference of more
informative types (and issuing more informative error messages).
For example, overloading and using "first" on pairs and triples:
In Haskell
______________________________________________
| class First p a where |
| first:: p -> a |
| |
| instance First (a,b) a where |
| first = fst |
| instance First (a,b,c) where |
| first (a,b,c) = a |
| |
| f x y = first (x,y) |
| main = print ((f::Bool->Int->Bool) True 10) |
|_____________________________________________|
In CT
____________________________
| fst (a,b,c) = a | Type inferred for f:
| | in CT: a -> b -> a
| f = curry fst | in Haskell:
| main = print (f True 10) | First (a,b) c => a -> b -> c
|__________________________|
Constraints on types are maintained intenally but, since they are
inferred, in interaction with programmers in system CT can
use only simple (unconstrained) types.
-- Open World and Autonomous Software Components (somewhat ortogonal
issue, not yet implemented in this prototype)
Support for the use of type annotations, instead of import clauses,
extends the open world approach for supporting the construction of
autonomous software components (and mutually recursive modules).
For example, one could use, instead of
import Monad
the following:
assume (return:: a -> m a,
(>>=) :: m a -> (a -> m b) -> m b)
or equivalently:
assume MonadInterface
Yours,
Carlos
