Carlos Camarão

Lucilia Figueiredo

 

 

System CT

 

Features

Papers

Software and Examples

 

 

Other references

 

 

 

SYSTEM CT: Constrained Types for Overloading

Research Project

 

 

People:  Carlos Camarão  - DCC-UFMG  

photo     Lucilia Figueiredo – DECOM UFOP

            Cristiano Damiani Vasconcellos – PUC-PR

(top)

System CT:

System CT extends ML-style type inference for supporting overloading and polymorphic recursion. The simplicity of core-ML type inference is maintained, with no exception or special constructs included for coping with overloading.

(top)

Features:

The aim of this project is to define and implement a type inference algorithm for a language with support for overloading and polymorphic recursion, with the following features:

  1. No conflict with data abstraction: To introduce no conflict between data abstraction and types of overloaded symbols, constraints on types of overloaded symbols must be automatically inferred, and not be determined a priori by programmers, according to which overloaded symbols are used (an implementation-dependent issue).

 

Haskell 

 

class Collection c where 

   ... 

   member:: Eq a => a -> c a -> Bool 

   ... 

instance Colletion Set where 

   ... 

   member ... = ... 

   ... 

CT 

 

   ---

   ... 

member:: {...} => a -> Set a -> Bool 

   ... 

   ... 

  member ... = ... 

   ... 

1.      No class and instance declarations

2.      No constraints required in type annotations: "{...}" remarks that a type error results if "overloaded symbols in this expression are not used appropriately"

3.      No mandatory type annotation

4.      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)

 

2.     Generality: Support of overloading of constants and functions, including overloading of 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 simply overloading map:

map f (Leaf a) 

= Leaf (f a) 

map f (Node a b) 

= Node (map f a) (map f b) 

3.     Simple and informative types: ML-style type inference and ad-hoc overloading in a "closed world" means that types are inferred according to visible definitions, resulting in more informative types and error messages. For example, overloading and using ``first'' on pairs and triples:

 

Haskell 

class First p a where 

   first:: p -> a 

 

instance First (a,b) a where 

   first = fst 

 

instance First (a,b,c) a where 

   first (a,b,c) = a 

 

f x y = first (x,y

main = print ((f::Int->Int->Int) 1 2) 

 

  Type inferred for f :

    First (a,b) c => a -> b -> c 

CT 

 

fst (a,b,c

= a 

= curry fst 

main 

= print (f 1 2)

 

 

 

 

 

 

 

 

 

 

    Type inferred for f :

       {...} => a -> b -> a 

 

  1. Constraints on types, which contain information about the set of overloaded symbols used in a given definition, are maintained internally but, since they are inferred, instead of being required in annotations made by programmers, System CT can interact with the programmer by means of simple, unconstrained types.

5.     Autonomous software components: Support for the use of type annotations, instead of import clauses, enable the construction of autonomous software components (and mutually recursive modules). For example, one could use:

instead of

the following:

or, equivalently:

 

import Monad

 

assume

return 

:: a -> m a 

 

(>>=) 

:: m a -> (a -> m b) -> m b 

 

... ) 

 

 

assume MonadInterface

 

(top)

Papers:

1.     [1] Constraint-set Satisfiability for Overloading (.pdf), Carlos Camarão, Lucília Figueiredo, Cristiano Vasconcellos, Proceedings of 6th ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming, Verona, Italy, August 24-26, 2004.

2.     [2] Practical Type Inference for Polymorphic Recursion: an Implementation in Haskell  (ps.gz), Cristiano VasconcellosLucília Figueiredo, Carlos Camarão, Proceedings of SBLP'2003 - VII Brasilian Symposium on Programming Languages, Ouro Preto, MG, Brasil, May 2003, in Journal of Universal Computer Science, volume 9(8), 2003. available at http://www.jucs.org/jucs_9_8.

3.     [3] Type Inference for Overloading  (ps.gz), Carlos Camarão, Lucília Figueiredo, Technical Report, December, 2002.

4.      [4] Principal Typing and Mutual Recursion, Lucília Figueiredo, Carlos Camarão, International Workshop on Functional and Logic Programming (WFLP'2001), Kiel, Germany, September 13-15, Technical Report No. 2017 of the University of Kiel, 2001.

(top)

Software and examples:

Cristiano Damiani Vasconcellos has implemented (as part of his Phd) a front-end for a mini-Haskell without type classes and with support for free ad-hoc polymorphism as allowed in system CT. The implementation is available, with examples, here. Another version (with a monadic parser, that doesn't need Happy and other stuff...) is available here. The implementation is mainly an adaptation of System CT to deal with mutual recursion in binding groups [2]. Constraint-set satisfiability is implemented as described in [1].

The system/type inference algorithm does not need the type annotations given in Haskell's class and instance declarations, and constraints (contexts) need never be specified in type annotations (since they are automatically inferred). The inference of more informative types is due to the use of a closed world. I am confident that the use of this form of constrained polymorphism will bring some benefits, specially related to generic programming.

Comments, suggestions etc., please contact:  Carlos Camarão   or   Lucília Figueiredo

 

(top)

Other references:

 

 

 

Computer Science Department

Federal University of Minas Gerais                        (last modified:  23/11/2004)