20 lines
484 B
Text
20 lines
484 B
Text
(* every object is basically a trait, just an interface *)
|
|
(* partial decomposition is possible *)
|
|
|
|
(* lets build a simple stack *)
|
|
|
|
λ $blti → {
|
|
|
|
pub let maybe = λ $T → data { :null; } λ $ →
|
|
.{ .none = blti.unitTy; .some = blti.boxTy T; };
|
|
|
|
let stack_ds = λ $T → μ $sdst → maybe (^{ T; sdst });
|
|
|
|
pub let stack = λ $T → {
|
|
let sdst = stack_ds T;
|
|
pub let nil = sdst.none blti.unit;
|
|
pub let push = λ $xs → λ $x →
|
|
sdst.some (blti.box .{ x; xs });
|
|
};
|
|
|
|
}
|