type nat = +{'zero : 1, 'succ : nat}
type pos = +{           'succ : nat}

type pstream = <nat * padding> (* a padded stream *)

(* finite, positive padding *)
type padding = +{'none : padding, 'some : [pstream]}
type zstream = <nat * +{'some : [zstream]}>

comp compress : [pstream] -> zstream
   = fun x0 => let <x1> = force x0 in
               match x1 { (x2,x3) => <x2, 'some [skip x3]> }
comp skip : padding -> zstream
   = fun x0 => match x0 { 'none x1 => skip x1
                        | 'some x2 => compress x2 }
(* evaluate *)
eval stream0 : pstream
   = <'zero (), 'none 'none 'none 'some [stream0]>
eval stream1 : zstream
   = compress [stream0]

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