Re: [TYPES] I'm searching for a survey on type system feature combinations

[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

On 15/06/15 05:08, [email protected] wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]

> I was wondering if there exists a comprehensive survey somewhere that
> covers how different type system features interact with each other. The
> only one I know of is Barendregt's Lambda Cube -- each axis of the cube is
> a different "feature" and each vertex corresponds to a different
> combination of features. However, the Lambda Cube doesn't cover things
> like subtyping, mutable references, intersection/union types, etc. Is
> there something out there that does?
>



It is not a survey but if you want an actual language that uses
subtyping, mutable references, union/intersection/negation types, then
you can try CDuce (http://www.cduce.org) that is included in all major
Linux distributions. The reference paper for the language was presented
at ICFP 2003.

Actually you can also try it with parametric polymorphism (reference
papers in POPL 2014 and POPL 2015 : Polymorphic functions with
set-theoretic types) but since polymorphism is not included in the
distribution, yet, you have to compile the alpha version available at
https://www.cduce.org/redmine/projects/cduce

Cheers

Beppe


P.S.
If you wonder about the advantages of using union and intersection types
with polymorphism here you are Okasaki' s implementation of red-black
trees balance and insert: thanks to intersection types you can
statically enforce that red-nodes have only black children (AFAIK you
need GADTs to do it in ML).

(* RedBlack tree *)
type RBtree('a) = Btree('a) | Rtree('a)

(* Black rooted RB tree: a leaf or a black node *)
type Btree('a) = [] | <black elem='a>[ RBtree('a) RBtree('a) ]

(* Red rooted RB tree: only black childs *)
type Rtree('a) = <red elem='a>[ Btree('a) Btree('a) ]

(* Wrongtree : a red tree with a red child *)
type Wrongtree('a) =    <red elem='a>( [ Rtree('a) Btree('a) ]
                                      | [ Btree('a) Rtree('a) ])

(* Unbalanced : a black node with a wrong tree child *)
type Unbalanced('a) = <black elem='a>( [ Wrongtree('a) RBtree('a) ]
                                      | [ RBtree('a) Wrongtree('a) ])
;;


(* Balance is a function that when applied to a unbalanced tree *)
(* it returns a red tree and when applied to something that is  *)
(* not unbalanced, it returns a result of the same type.           *)
(* balance : (Unbalanced('a) -> Rtree('a)) /\                   *)
(*           ('b\Unbalanced(Any) -> 'b\Unbalanced(Any))         *)

let balance ( Unbalanced('a) -> Rtree('a) ; 'b\Unbalanced(Any) -> 
'b\Unbalanced(Any) )
   | (<black (z)>[ <red (y)>[ <red (x)>[ a b ] c ] d ]
   | <black (z)>[ <red (x)>[ a <red (y)>[ b c ] ] d ]
   | <black (x)>[ a <red (z)>[ <red (y)>[ b c ] d ] ]
   | <black (x)>[ a <red (y)>[ b <red (z)>[ c d ] ] ]) & Unbalanced(Any) ->
         <red (y)>[ <black (x)>[ a b ] <black (z)>[ c d ] ]
   | x -> x
;;


(* insert: 'a -> Btree('a) -> Btree('a)\[]                      *)
(* it preserves the type and returns a non empty tree           *)

let insert (x : 'a) (t : Btree('a)) : Btree('a)\[] =
   let ins_aux ( [] -> Rtree('a);
                 Btree('a)\[] -> RBtree('a)\[];
                 Rtree('a) -> Rtree('a)|Wrongtree('a) )
     | [] -> <red elem=x>[ [] [] ]
     | (<(color) elem=y>[ a b ]) & z ->
            if x << y then balance <(color) elem=y>[ (ins_aux a) b ]
        else if x >> y then balance <(color) elem=y>[ a (ins_aux b) ]
        else z

(* if ins_aux is applied to a leaf it returns a red tree, to a  *)
(* black node it returns a non-empty RBtree, a red node it      *)
(* returns either a red tree of a wrongtree to be balanced.     *)