diff --git a/nt/primitives/examples/maybe.nix b/nt/primitives/examples/maybe.nix new file mode 100644 index 0000000..edccf34 --- /dev/null +++ b/nt/primitives/examples/maybe.nix @@ -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; + }; +} diff --git a/nt/primitives/examples/rose.nix b/nt/primitives/examples/rose.nix new file mode 100644 index 0000000..9a9fa4d --- /dev/null +++ b/nt/primitives/examples/rose.nix @@ -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: { ... }); +}