system-f.srpt

let func = \X (\c: {None | Some X}. \x: X->(X, X). 
	case c of 
		| None => None of {None | Some (X, X)}
		| Some val => Some x val of {None | Some (X, X)} )
in func [Nat] (Some 10 of {None|Some Nat}) (\x: Nat. (x, x))
;

let poly = \X \x: X. x in 
	let x = poly [Nat] 0 in 
	let y = poly [Bool] false in 
	let z = poly [(Nat, Bool)] in 
	z (x, y)
;

let poly = \X \Y (\func: X->Y. \val: X. func val) in poly [Nat][Bool]
;


case Some (5, 2) of {None | Some (Nat, Nat)} of 
 | None => (0, 0)
 | Some (1, _) => (1, 1)
 | Some(x, y) => (y, x)
;

case (1, (2, 3)) of 
	| (x, (y, z)) => ((z, y), x)
;
let x = 
	\z: (Nat, Nat)->Nat. 
		\y: (Nat, Nat).
			case y of
				| (0, x) => x,
				| x => z (pred y.0, succ (succ x.1))
	in (fix x) (10, 0)

;

let cdr = \list: NatList. 
	case unfold NatList list of 
		| Nil => Nil of NatList
		| Cons (x, xs) => xs
in cdr Cons (10, Cons (20, Nil of NatList) of NatList) of NatList
;

case unfold NatList Cons (10, Cons (20, Nil of NatList) of NatList) of NatList of 
	| Nil => Nil of NatList 
	| Cons (10, xs) => Cons (11, xs) of NatList
	| Cons (x, xs) => xs
;

let nil = Nil of NatList in 
let cons = (\val: Nat. \list: NatList. Cons (val, list) of NatList) in
case unfold NatList (cons 1 nil) of 
	| Nil => nil
	| Cons (x, y) => y

;

let x = 10 in let (y, _) = (x, 1) in y;

let (x, y) = (0, 10) in let z = x in z ;

(\x: Nat. \Y \y: Nat->Y. y x) 10 [Nat] succ
;

let x = (\struct: (Nat, Nat, Nat). 
	let (_, q, _) = struct
	in q) in
	x (10, 12, 13)

let x = \A \B \C \tuple: (A, B, (C, C)).
	let (_, mid, (n, s)) = tuple in 
	(n, mid, s, mid) in
	x [Nat] [Bool] [Nat] (10, true, (1, 11))
;

let package = (pack Nat, ((\x: Nat. succ (succ x)), 0) as exists X. (X->Nat, X)) in
	unpack package as T, mod in mod.0 ((\x: T. x) mod.1)
;

let package = (pack Bool, ((\x: Bool. case x of | true => 10 | false => 0), true) as exists REPR. (REPR->Nat, REPR)) in
let x = (\x: exists T. (T->Nat, T). unpack x as T, mod in succ (mod.0 mod.1)) in
	x package 
;