type nat = +{'zero : 1, 'succ : nat}
type bin = +{'e : 1, 'b0: bin, 'b1 : bin}
type std = +{'e : 1, 'b0: pos, 'b1: std}
type pos = +{        'b0: pos, 'b1: std}

(* a fn that increment nats and bins *)
comp inc : nat -> <nat> /\ bin -> <bin>
   = fun x0 => match x0 {  'e u => <'b1 'e u>
                        | 'b0 x1 => <'b1 x1>
                        | 'b1 x2 => let <x3> = inc x2 in <'b0 x3>
                        | 'zero _ => <'succ x0>
                        | 'succ _ => <'succ x0> }
(* evaluate nat(s) *)
eval one : <nat> = <'succ 'zero ()>
eval two : <nat> = let <x> = one in inc x
eval ten : <pos> = <'b1 'b0 'b1 'e ()>
(* evaluate inc with pos (pos is a subtype of nat) *)
eval eleven : <bin> = let <x> = ten in inc x

Generated by Zeeshan Lakhani using scpaste at Sat Aug 10 01:35:17 2024. EDT. (original)