26 lines
602 B
Text
26 lines
602 B
Text
(*
|
|
* SPDX-FileCopyrightText: 2023 Alain Zscheile <fogti+devel@ytrizja.de>
|
|
*
|
|
* SPDX-License-Identifier: CC0-1.0
|
|
*)
|
|
(* 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 });
|
|
};
|
|
|
|
}
|