my vision
This commit is contained in:
parent
9ee4ae5f29
commit
6537f0cdaa
2 changed files with 143 additions and 0 deletions
68
nt/primitives/examples/maybe.nix
Normal file
68
nt/primitives/examples/maybe.nix
Normal file
|
|
@ -0,0 +1,68 @@
|
||||||
|
{this, ...}: let
|
||||||
|
inherit
|
||||||
|
(this)
|
||||||
|
ntTrapdoorKey
|
||||||
|
ntDynamicTrapdoorKey
|
||||||
|
mkTrapdoorFn
|
||||||
|
mkTrapdoorSet
|
||||||
|
;
|
||||||
|
in {
|
||||||
|
# NOTE: Maybe is used to simplify parsing Type/Class declarations
|
||||||
|
# NOTE: and therefore must be implemented manually
|
||||||
|
Maybe = let
|
||||||
|
meta = instance: {
|
||||||
|
sig = "nt::&Maybe";
|
||||||
|
derive = [];
|
||||||
|
ops = {};
|
||||||
|
req = {"nt::&Maybe" = ["unwrap"];};
|
||||||
|
};
|
||||||
|
in
|
||||||
|
mkTrapdoorFn {
|
||||||
|
default = {
|
||||||
|
unwrap = "TODO";
|
||||||
|
};
|
||||||
|
unlock.${ntTrapdoorKey} = meta false;
|
||||||
|
};
|
||||||
|
|
||||||
|
Some = let
|
||||||
|
meta = instance: {
|
||||||
|
inherit instance;
|
||||||
|
sig = "nt::Some";
|
||||||
|
derive = ["nt::&Maybe"];
|
||||||
|
ops = {
|
||||||
|
"nt::&Maybe".unwrap = f: self: f self.${ntDynamicTrapdoorKey}.value;
|
||||||
|
};
|
||||||
|
req = {};
|
||||||
|
};
|
||||||
|
in
|
||||||
|
mkTrapdoorFn {
|
||||||
|
default = value:
|
||||||
|
mkTrapdoorSet {
|
||||||
|
unlock = {
|
||||||
|
${ntTrapdoorKey} = meta true;
|
||||||
|
${ntDynamicTrapdoorKey} = {
|
||||||
|
inherit value;
|
||||||
|
};
|
||||||
|
};
|
||||||
|
};
|
||||||
|
unlock.${ntTrapdoorKey} = meta false;
|
||||||
|
};
|
||||||
|
|
||||||
|
None = let
|
||||||
|
meta = instance: {
|
||||||
|
inherit instance;
|
||||||
|
sig = "nt::None";
|
||||||
|
derive = ["nt::&Maybe"];
|
||||||
|
ops = {
|
||||||
|
"nt::&Maybe".map = f: self: self;
|
||||||
|
};
|
||||||
|
req = {};
|
||||||
|
};
|
||||||
|
in
|
||||||
|
mkTrapdoorFn {
|
||||||
|
default = mkTrapdoorSet ntTrapdoorKey {
|
||||||
|
unlock = meta true;
|
||||||
|
};
|
||||||
|
unlock.${ntTrapdoorKey} = meta false;
|
||||||
|
};
|
||||||
|
}
|
||||||
75
nt/primitives/examples/rose.nix
Normal file
75
nt/primitives/examples/rose.nix
Normal file
|
|
@ -0,0 +1,75 @@
|
||||||
|
{
|
||||||
|
nib,
|
||||||
|
# typespace,
|
||||||
|
...
|
||||||
|
}: let
|
||||||
|
inherit
|
||||||
|
(nib)
|
||||||
|
Attrs
|
||||||
|
Bool
|
||||||
|
contains
|
||||||
|
expect
|
||||||
|
flipCurry
|
||||||
|
Fn
|
||||||
|
getHidden
|
||||||
|
Meta
|
||||||
|
PartialOrder
|
||||||
|
Prod
|
||||||
|
Sum
|
||||||
|
Type
|
||||||
|
Class
|
||||||
|
UnFn # UnFn = Fn Any Any
|
||||||
|
;
|
||||||
|
in {
|
||||||
|
# Rose = Struct "nib::Rose" (Rose: {
|
||||||
|
Rose = Type "nib::Rose" (Self: {
|
||||||
|
ops = {
|
||||||
|
# elements can either be an attribute set, or a function/lambda
|
||||||
|
# roses :: [Rose]
|
||||||
|
Type.mk = meta: roses: {
|
||||||
|
expose = roses;
|
||||||
|
hidden = {inherit meta;};
|
||||||
|
};
|
||||||
|
|
||||||
|
PartialOrder.leq = flipCurry contains;
|
||||||
|
|
||||||
|
Meta.get = R: (getHidden R).meta;
|
||||||
|
};
|
||||||
|
|
||||||
|
derive = [
|
||||||
|
PartialOrder
|
||||||
|
Meta
|
||||||
|
];
|
||||||
|
});
|
||||||
|
|
||||||
|
PartialOrder = Class "nib::&PartialOrder" (Self: {
|
||||||
|
ops = {
|
||||||
|
# NOTE: `Prod A B` == `Prod [A B]`
|
||||||
|
leq = expect <| Fn (Prod Self Self) Bool;
|
||||||
|
gt = ! Self.leq;
|
||||||
|
};
|
||||||
|
});
|
||||||
|
|
||||||
|
Meta = Class "nib::&Meta" {
|
||||||
|
# NOTE: `Sum A B` == `Sum [A B]`
|
||||||
|
attrs.hidden.meta = expect <| Sum [UnFn Attrs];
|
||||||
|
ops.get = T: (getHidden T).meta;
|
||||||
|
};
|
||||||
|
|
||||||
|
ProperType = Class "nib::&ProperType" (Self: {
|
||||||
|
ops.mk = expect <| Sum [UnFn Self];
|
||||||
|
});
|
||||||
|
|
||||||
|
Trivial =
|
||||||
|
Class "nib::&Trivial" {
|
||||||
|
};
|
||||||
|
|
||||||
|
# We can now do the following:
|
||||||
|
# `Rose.mk meta [...]` <-> `Rose meta [...]`
|
||||||
|
# Rose.leq roseA roseB
|
||||||
|
# Rose.meta roseA
|
||||||
|
# Rose.verify # Verify all Axioms
|
||||||
|
|
||||||
|
# in Cerulean: (Nix-style type extensions via overlays/overrides)
|
||||||
|
# Group = nib.overrideStruct Rose (prev: { ... });
|
||||||
|
}
|
||||||
Loading…
Add table
Add a link
Reference in a new issue