talk.1ml

;; Types as modules

M1 = {type t = int} : {type t = int} :> {type t};
M2 = {t = type int} : {t : (= type int)} :> {t : type};
M3 = (type int) : (= type int) :> type;


;; Type constructors as applicative functors

M = { type point a = {x : a; y : a} };
M = { point = fun (a : type) => type {x : a; y : a}; };

type S = { type point a };
type S = { point : (a : type) => type };

type T = { type point a = {x : a; y : a} };
type T = { point : (a : type) => (= type {x : a; y : a}) };

M' = M : S;
M'' = M :> T;


;; Map functor (explicitly typed)

type EQ =
{
  type t;
  eq : t -> t -> bool;
};

type MAP =
{
  type key;
  type map a;
  empty a : map a;
  lookup a : key -> map a -> opt a;
  add a : key -> a -> map a -> map a;
};

Map (Key : EQ) :> MAP with (type key = Key.t) =
{
  type key = Key.t;
  type map a = key -> opt a;
  empty (a : type) = fun (x : key) => none;
  lookup (a : type) (x : key) (m : map a) = m x;
  add (a : type) (x : key) (y : a) (m : map a) =
    fun (z : key) => if Key.eq z x then some y else m z : opt a;
};


;; Map functor (implicitly typed)

type MAP =
{
  type key;
  type map a;
  empty 'a : map a;
  lookup 'a : key -> map a -> opt a;
  add 'a : key -> a -> map a -> map a;
};

Map (Key : EQ) :> MAP with (type key = Key.t) =
{
  type key = Key.t;
  type map a = key -> opt a;
  empty = fun x => none;
  lookup x m = m x;
  add x y m = fun z => if Key.eq z x then some y else m z;
};


;; Higher-rank polymorphism

f (id : 'a => a -> a) = (id 5, id "text");


;; Asociated types

type COLL c =
{
  type key;
  type val;
  empty : c;
  add : c -> key -> val -> c;
  lookup : c -> key -> opt val;
  keys : c -> list key;
};

entries 'c (C : COLL c) xs : list (type (C.key, C.val)) =
  List.map (C.keys xs) (fun k => caseopt (C.lookup xs k) bot (fun v => (k, v)));


;; Higher-kinded polymorphism

type MONAD (m : type => type) =
{
  return 'a : a -> m a;
  bind 'a 'b : m a -> (a -> m b) -> m b;
};

map 'a 'b (m : type => type) (M : MONAD m) (f : a -> b) mx =
  M.bind mx (fun x => M.return (f x));

do map :
  'a => 'b => (m : type => type) => (M : MONAD m) => (a -> b) -> m a -> m b;


;; Objects

type point' self =
{
  getX : () -> int;
  getY : () -> int;
  move : int -> int -> self;
};
type recpoint = rec (x : type) => point' x;
type point = point' recpoint;

newpoint = rec (newpoint : int -> int -> point) => fun x y =>
{
  getX () = x;
  getY () = y;
  move dx dy = @recpoint (newpoint (x + dx) (y + dy));
};

p = newpoint 3 4;
p' = p.move 1 2 .@recpoint;
do Int.print (p'.getX ());
do print " ";
do Int.print (p'.getY ());
do print "\n";


;; Computed modules

;; couple of dummies...
datasize = 117;
OrderedMap = Map {include Int; eq = curry (==)} :> MAP;
HashMap = Map {include Int; eq = curry (==)} :> MAP;

Map = if datasize <= 100 then OrderedMap else HashMap : MAP;