Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-01-21 18:25:53 -0800 (Fri, 21 Jan 2005)
Revision: 6469
Log message:
Added sequent types (but no sequent type checking yet).
Here are some invariants.
Typeclasses, declaring a new class class1.
declare class1 <- class2
-- Any term in class2 is also in class1.
declare class1 -> class2
-- Any term in class1 is also in class2.
declare class1
-- No subtyping relationship.
-- The term << class1 >> has type << type >>.
-- The term << class1 >> has typeclass << class1 >>.
Type declarations, declaring a new type << ty{'a; 'b; 'c} >>.
declare type ty{'a; 'b; 'c} : tc
-- The term << ty{'a; 'b; 'c} >> has type << type >>
-- The term << ty{'a; 'b; 'c} >> has typeclass << tc >>
declare type ty{'a; 'b; 'c}
-- The term << ty{'a; 'b; 'c} >> has type << type >>
-- The term << ty{'a; 'b; 'c} >> has typeclass << term >>
Term declarations:
declare t[typedparams]{typed_bterms} : ty
Typed items include : constraints. Consider the following
for example.
declare typeclass foo -> term
declare type list{'a : type} : foo
declare nil : list{'a}
declare cons{'hd : 'a; 'tl : list{'a}} : list{'a}
If a constraint is missing, the type is << term >> by default.
The term << list{'a : type} >> is a type for any type << 'a >>,
and << nil >> and << cons{'hd; 'tl} >> have the expected types.
Also, << nil >> and << cons{'hd; 'tl} >> have typeclass << foo >>,
which is included in << term >>.
The terms << foo >> and << list{'a} >> have type << type >>.