Rewrite meta-check.nix type checking logic.

[Profpatsch]

Description of the main commit:

stdenv/generic/check-meta: rewrite type checking code  …
The previous code used some ad-hoc attribute enumeration to check for missing
fields and did not really type check the attributes, because it used `t.check`
from the module system types, which only does shallow checks for nested types,
e.g. just `builtins.isList` for (listOf strings).

This new version uses `types-simple` to recursively check every attribute,
outputting accurate information for type errors in nested fields, e.g.:

Package ‘hello-2.10’ in … has an invalid meta attrset:
maintainers.1.email should be: string
but is: null

When we set
meta.maintainers [ eelco foobar ];
in `hello/default.nix` and foobar is defined as
{ name = "foobar"; email = null; };
in `maintainers-list.nix`.

The path accurately pins down where the type check failed:
In the `maintainers` field, the second element of the list (counting from 0)
and the field email in that element.

Further work: If an unsupported meta field is used, the type error will print
the complete type of the meta product, which is quite big. The type error should
show a diff of the problematic fields in that case.
This is possible but not yet integrated into the type checking logic.

Please go trough the commits one-by-one, since they all add some pretty different changes and are built on each other as single units.
Adding the type library might be a bit controversial, but I hope I have provided enough incentive in the docstrings and the commit messages to persuade you that it is a good addition.

Meta can be checked with this invocation from the ofborg readme.

[Profpatsch]

Okay, with the latest commit I recommend looking at lib/types-simple.nix in the overview, since it should be a lot easier to understand with these comments.

[aszlig]

Great work on the type system, although I'm not quite sure whether this is a good idea to use for checking meta, because we already have to fight against eval time.

Apart from that, it could also make sense to replace the type checking for the NixOS module system to use this instead (as it avoids the need to use tryEval for checking) on everything but submodules, maybe @nbp could chime in for that as well.

Other than that, I think adding another type system needs to have more eyes on this, so I'd suggest adding this as a separate pull request.

[aszlig]

Why not concatLists (which is a primop)?

[Profpatsch]

Good catch, will change.

[aszlig]

Did you actually measure the evaluation time overhead this has?

[Profpatsch]

Nope, how would I measure it? Maybe cc @grahamc.

Right now the checks are not enabled by default, of course that would be a final goal.

[aszlig]

This is not used anywhere, maybe remove?

[aszlig]

So why have it in the first place?

[Profpatsch]

Ah, it’s used in the tests for example: (list void) is a type with exactly one inhabitant, []. One wouldn’t believe it, but void is a pretty handy type to have (the description is a bit tongue-in-cheek).

[aszlig]

Why do we need this type?

[Profpatsch]

Similar to void this doesn’t seem useful at first, but it’s even more elementar than bool in a sense; e.g. the void you find in languages like C(++) is really a unit.

A great use-case is for sum types:

let mode = sum { off = unit; level = int; };
in checkType mode { off = {}; }

which corresponds to the Haskell type:

data Mode = Off | Level Int

[aszlig]

Maybe call this listOf so we use the same naming as with NixOS modules.

[Profpatsch]

I deliberately changed the names to be internally consistent; the module system has string and str, because string did strange concatenation. listOf and attrsOf have the same history with attrs and list, which are not able to recursively check their contents.

Compare the correspondence table below.

[aszlig]

Same here: attrsOf

[aszlig]

I'd use intersectAttrs (especially because it's a primop) here instead of converting to list and use subtractLists.

[Profpatsch]

To check for then reqfs == vfs in the line below, I’d have to use builtins.intersectAttrs v req == req, which has to do a deep equality check for req (or v if I turn the arguments around).

[aszlig]

Hm, I don't think this has any more benefit to having to specify the defaults directly, especially if it comes to code readability. You need to look up the default here instead of just following the code you're already looking at.

[Profpatsch]

I implemented that as a crutch for optional fields originally, but productOpt kind of replaced it pretty quickly. It might make sense to remove it again, yes.

[Profpatsch]

Here’s a (non-exhaustive) correspondence table.

module types	types-simple
string	n/a
str	string
attrs	attrs any
list	list any
attrsOf	attrs
listOf	list
either l r	union [ l r ]
loaOf t	union [ (list t) (attrs t) ]
nullOr	n/a
submodule	~ product/productOpt
enum	can be trivially built with restrict
ints.between	can be trivially built with restrict
n/a	sum
addCheck (no description update)	restrict

Some of the module types come from the fact that they also contain merging logic and submodule logic, which complicates the base design and lead to the deprecation of some types.

[Profpatsch]

Okay, rebase onto current master after the changes in check-meta.nix.

@Ericson2314 I noticed you create a lot of types in lib/system/parse.nix. I think changing the checks to lib.types-simple from this pull request would improve the type errors as well as how concise these types work (after adding an enum type). For now I’ve stubbed the meta.platforms fields out with any.

[Profpatsch]

@Ericson2314 This is where I stub out the platform types at the moment.

[Profpatsch]

Update: enum and other restricted types are now possible using restrict.

[edolstra]

Please use camelCase for attribute names.

[edolstra]

What is the memory / evaluation time impact of this?

[edolstra]

What are "products"? Seems like a pretty strange terminology.

[Nadrieril]

types-simple is essentially defining algebraic data types, like ML or Haskell have; "products" is the standard terminology for tuple- or record-like things in this setting.

[oxij]

A couple of clarifications. In

I think `types-simple` should replace `types`

I mean that either `types-simple` should expose the merging NixOS modules would use, or `types` should `types-simple` for type checking. In

without duplicating already inferable information

and related I mean the following kind of duplication ```imaginary-typed-nix option :: builtintypes.str option = mkOption { merge = types.str.merge; }; ``` Similarly, in

a semantically very different nix

and related I also mean that it's unclear how you would typecheck ```nix { require = [ <module that defines `option`> ]; config = { option = value; }; } ``` without merging NixOS modules and nix (currently non-existent) modules into a single concept. Also, an idea I wanted to use when I planned implementing pretty much the same thing: I planned to make `bool` into a non-mergable bool and split other uses into `types.any` and `types.all` since `bool` has two different monoids. E.g. you would then use `all` for normal `enable` options (because if somebody disabled it, they probably know what they are doing, why make them use `mkForce`?) and `any` for security-related options (because to make things insecure everyone should agree).

[Profpatsch]

I planned to make bool into a non-mergable bool and split other uses into types.any and types.all since bool has two different monoids.

Ah, the Monoid remark is enlightening, yes. Merging is really just <> (the binary operator) and defaults are mempty, (the one-element). Awesome!

[oxij]

ping! Progress? Do you have an updated/rebased version of this to play with?

[Profpatsch]

@oxij I have just pushed a branch which does away with the in-file changes of check-meta.nix and gives you a type that can check derivation & meta fields: Profpatsch@7a2caa0

I intend to commit all improvements to that branch (types-simple-standalone) first.

[oxij]

@Profpatsch awesome, thanks!

[Nadrieril]

Wow, this is great work ! I really like having the typeckecking logic separate from the merging logic. Is there a plan to make nixos types use this for typechecking under the hood ?

[Shados]

@Profpatsch this is perhaps somewhat off-topic, but I read through types-simple.nix, and I found it rather tricky to understand the actual type checking code. Primarily, pulling the recursion out of checkType and into cata and fmap made the control flow egregiously difficult for me to follow, and fmap effectively changing the semantics of the nested types in-place was unexpected. In order to understand it, I ended up having to write a version of it wihout either of those.

From the context, I gather that the design is based on ideas from category theory, and would (I assume) be easily comprehensible to people familiar with it. As a result, I am curious: are there other benefits in this specific instance to keeping the implementation so close to the abstract design?

Those comments notwithstanding, I still found it easier to understand than the existing module type system, and having a self-contained type system in place would be very useful.

[Profpatsch]

From the context, I gather that the design is based on ideas from category theory

No, not really, it’s from the classic bananas & barbed wire paper. You can find an explanation here: http://reasonablypolymorphic.com/blog/recursion-schemes/
It helps greatly when dealing with recursive data structures, by splitting open their recursion and just looking at one layer at a time.
You are right that it superficially complicates the code in an untyped setting, but in practice it is a great fit for a type checker which is intended to be expanded by users. If I expose the alg definition in checkType (which I should totally do), users can chain new transformations to each layer of recursion, e.g. to change error messages according to their needs.

[mmahut]

Are there any updates on this pull request, please?

[Profpatsch]

Are there any updates on this pull request, please?

I still think it’s valuable, but I don’t know of any way out of the “we don’t want two type systems in nixpkgs” issue.

[stale]

Thank you for your contributions.
This has been automatically marked as stale because it has had no activity for 180 days.
If this is still important to you, we ask that you leave a comment below. Your comment can be as simple as "still important to me". This lets people see that at least one person still cares about this. Someone will have to do this at most twice a year if there is no other activity.
Here are suggestions that might help resolve this more quickly:

1. Search for maintainers and people that previously touched the
   related code and @ mention them in a comment.
2. Ask on the NixOS Discourse. 3. Ask on the #nixos channel on
   irc.freenode.net.