diff options
author | Vincent Ambo <github@tazj.in> | 2019-08-08T01·15+0000 |
---|---|---|
committer | Vincent Ambo <tazjin@google.com> | 2019-08-28T13·35+0100 |
commit | fe33a82a072bfe657f509bd9b7d756f10a92817f (patch) | |
tree | 309c6f4ad2b9bca681032511e88bfb7aa61ab87d |
feat: Initial check-in of type system sketch
-rw-r--r-- | yants.md | 16 | ||||
-rw-r--r-- | yants.nix | 88 |
2 files changed, 104 insertions, 0 deletions
diff --git a/yants.md b/yants.md new file mode 100644 index 000000000000..dcdea0bd38f7 --- /dev/null +++ b/yants.md @@ -0,0 +1,16 @@ +yants +===== + +This is a tiny type-checker for data in Nix, written in Nix. It doesn't have all the features I think it should have (yet), but it works and its types are composable. + +## Primitives & simple polymorphism + +![simple](https://i.imgur.com/hDQAQUK.png) + +## Structs + +![structs](https://i.imgur.com/f8jgnul.png) + +## Nested structs! + +![nested structs](https://i.imgur.com/O3RsHds.png) \ No newline at end of file diff --git a/yants.nix b/yants.nix new file mode 100644 index 000000000000..feb3b8fd3410 --- /dev/null +++ b/yants.nix @@ -0,0 +1,88 @@ +# Provides a "type-system" for Nix that provides various primitive & +# polymorphic types as well as the ability to define & check records. +# +# All types (should) compose as expected. +# +# TODO: +# - error messages for type-checks of map/list elements are bad +# - enums? + +{ toPretty ? ((import <nixpkgs> {}).lib.generators.toPretty) }: + +# Checks are simply functions of the type `a -> bool` which check +# whether `a` conforms to the specification. +with builtins; let + # Internal utilities: + typeError = type: val: + throw "Expected type '${type}', but value '${toPretty {} val}' is of type '${typeOf val}'"; + + typedef = name: check: { + inherit name check; + __functor = self: value: + if check value then value + else typeError name value; + }; + + poly = n: c: { "${n}" = t: typedef "${n}<${t.name}>" (c t); }; + + poly2 = n: c: { + "${n}" = t1: t2: typedef "${n}<${t1.name},${t2.name}>" (c t1 t2); + }; + + typeSet = foldl' (s: t: s // (if t ? "name" then { "${t.name}" = t; } else t)) {}; + + # Struct checker implementation + # + # Checks performed: + # 1. All existing fields match their types + # 2. No non-optional fields are missing. + # 3. No unexpected fields are in the struct. + # + # Anonymous structs are supported (e.g. for nesting) by omitting the + # name. + checkField = def: value: current: field: + let + fieldVal = if hasAttr field value then value."${field}" else null; + type = def."${field}"; + checked = type.check fieldVal; + in if checked then (current && true) + else (throw "Field ${field} is of type ${typeOf fieldVal}, but expected ${type.name}"); + + checkExtraneous = name: def: present: + if (length present) == 0 then true + else if (hasAttr (head present) def) + then checkExtraneous name def (tail present) + else (throw "Found unexpected field '${head present}' in struct '${name}'"); + + struct' = name: def: { + inherit name def; + check = value: + let + fieldMatch = foldl' (checkField def value) true (attrNames def); + noExtras = checkExtraneous name def (attrNames value); + in (isAttrs value && fieldMatch && noExtras); + + __functor = self: value: if self.check value + then value + else (throw "Expected '${self.name}'-struct, but ${toPretty value} is of type ${typeOf value}"); + }; + + struct = arg: + if isString arg then (struct' arg) + else (struct' "anonymous" arg); +in (typeSet [ + # Primitive types + (typedef "any" (_: true)) + (typedef "int" isInt) + (typedef "bool" isBool) + (typedef "float" isFloat) + (typedef "string" isString) + + # Polymorphic types + (poly "option" (t: v: (isNull v) || t.check v)) + (poly "list" (t: v: isList v && (foldl' (s: e: s && (t.check e)) true v))) + (poly "attrs" (t: v: + isAttrs v && (foldl' (s: e: s && (t.check e)) true (attrValues v)) + )) + (poly2 "either" (t1: t2: v: t1.check v || t2.check v)) +]) // { inherit struct; } |