(continues from #nix-lang:nixos.org )
Matt Sturgeon:

you're asking a module system question, so NixOS Module System is more suitable 🙂

Ah! I didn't know about that channel. Thanks for pointing me here.

Either by shadowing check with submodule ... // { check = ...; } or extending it using lib.types.addCheck

Mh, I'd need to check how that works before I can fully understand that. Any reading material you suggest? Maybe there's a guide about internals of the modules type system.

Note that these may not work well with v2 check&merge (where checking is partly handled by the merge.v2 function).

No idea what v2 check&merge is, is that opt-in? Is something that's going in soon?

how should an empty module be handled?

None should match, type is a single-element enum with no default, so all of them should fail.

Right now I manually made a "union type" (where everything that a single type would allow, is allowed), and it has already bitten me.

bake.monorail: Thanks for asking this here. I have some similar ideas. This is currently a limitation of the type system.

We don't have explicit union discriminators.

Because we currently use check as union discriminator.
The check of a submodule is isAttrs x || isFunction x || path.check x so the first submodule type gets picked always.

There are some action points that i'd like to accomplish and one needs to figure out the order of them:

• Make oneOf the basetype of either. Currently inverted logic.
• Allow user defined explicit discriminators. Currently: implicitly reusing check def where we should do discriminator merged.value

bake.monorail: Thanks for asking this here. I have some similar ideas. This is currently a limitation of the type system.

We don't have explicit union discriminators.

Because we currently use check as union discriminator.
The check of a submodule is isAttrs x || isFunction x || path.check x so the first submodule type gets picked always.

There are some action points that i'd like to accomplish and one needs to figure out the order of them:

• Make oneOf the basetype of either. Currently inverted logic.
• Allow user defined explicit discriminators. Currently: implicitly reusing check def where we should do something along !merged.headError && discriminator merged.value

bake.monorail: Thanks for asking this here. I have some similar ideas. This is currently a limitation of the type system.

We don't have explicit union discriminators.

Because we currently use check as union discriminator.
The check of a submodule is isAttrs x || isFunction x || path.check x so the first submodule type gets picked always.

There are some action points that i'd like to accomplish and one needs to figure out the order of them:

• Document the limitations of the current system
• Make oneOf the basetype of either. Currently inverted logic.
• Allow user defined explicit discriminators. Currently: implicitly reusing check def where we should do something along !merged.headError && discriminator merged.value

I'd need to spend some time on the implementation of the modules system to be of some help.
I've no idea what the check function is, for instance.

I don't want to derail the discussion, but I'll just leave here my complaint that nix is lacking a type system and it's being reimplemented at run-time.
For instance, for "public API" functions I made up the following "type safe" function using the module system:

let
  typeSafeFunction =
    { options, implementation }:
    # Return a function that accepts some arguments
    arguments:
    # and invokes the implementation
    implementation
      # Passing as arguments the result of evaluating the module
      (pkgs.lib.evalModules {
        modules = [
          {
            inherit options;
            config = arguments;
          }
        ];
      }).config;
xxx = typeSafeFunction {
  options = { arg1 = mkOption { ...}; };
  implementation = { arg1 }: arg1 +1;
};
in
xxx { arg1 = 3; }

Which is a bit absurd.

It seems to me that the general feeling in the community is that nix won't get a type system any time soon. Maybe we need something like TypeScript, a TypeNix transpiler. I'm sure there already are some efforts like that.

I'd need to spend some time on the implementation of the modules system to be of some help.
I've no idea what the check function is, for instance.

I don't want to derail the discussion, but I'll just leave here my complaint that nix is lacking a type system and it's being reimplemented at run-time.
For instance, for "public API" functions I made up the following "type safe" function using the module system:

let
  typeSafeFunction =
    { options, implementation }:
    # Return a function that accepts some arguments
    arguments:
    # and invokes the implementation
    implementation
      # Passing as arguments the result of evaluating the module
      (pkgs.lib.evalModules {
        modules = [
          {
            inherit options;
            config = arguments;
          }
        ];
      }).config;
      xxx = typeSafeFunction {
        options = { arg1 = mkOption { ...}; };
        implementation = { arg1 }: arg1 +1;
      };
in
  xxx { arg1 = 3; }

Which is a bit absurd.

It seems to me that the general feeling in the community is that nix won't get a type system any time soon. Maybe we need something like TypeScript, a TypeNix transpiler. I'm sure there already are some efforts like that.

I'd need to spend some time on the implementation of the modules system to be of some help.
I've no idea what the check function is, for instance.

I don't want to derail the discussion, but I'll just leave here my complaint that nix is lacking a type system and it's being reimplemented at run-time.
For instance, for "public API" functions I made up the following "type safe" function using the module system:

let
  typeSafeFunction =
    { options, implementation }:
    # Return a function that accepts some arguments
    arguments:
    # and invokes the implementation
    implementation
      # Passing as arguments the result of evaluating the module
      (pkgs.lib.evalModules {
        modules = [
          {
            inherit options;
            config = arguments;
          }
        ];
      }).config;
  xxx = typeSafeFunction {
    options = { arg1 = mkOption { ...}; };
    implementation = { arg1 }: arg1 +1;
  };
in
  xxx { arg1 = 3; }

Which is a bit absurd.

It seems to me that the general feeling in the community is that nix won't get a type system any time soon. Maybe we need something like TypeScript, a TypeNix transpiler. I'm sure there already are some efforts like that.

Any reading material you suggest? Maybe there's a guide about internals of the modules type system.

Honestly, you'll get much more out of experiments with things like nix repl, nix eval (or nix-instantiate --eval), reading the relevant code in nixpkgs, etc.

I've no idea what the check function is, for instance.

The check function is what the module system uses to check "does this definition match this type". Every type has a check function.

$ nix repl
Nix 2.31.2+2
Type :? for help.
nix-repl> lib = import <nixpkgs/lib>

nix-repl> myType = lib.types.submodule {}

nix-repl> myType.check {}
true

nix-repl> myType.check ./file
true

nix-repl> myType.check ({ lib, ... }: {})
true

nix-repl> myType.check null
false

If you're curious about impl, you can use the repl to find where something is defined too:

nix-repl> builtins.unsafeGetAttrPos "check" myType
{
  column = 11;
  file = "/nix/store/ln4j1iqnnzs2ynx2cr88bdh65fmds2aq-source/lib/types.nix";
  line = 280;
}

nix-repl> :doc myType.check
Function __functor
… defined at
/nix/store/ln4j1iqnnzs2ynx2cr88bdh65fmds2aq-source/lib/types.nix:1271:32

Because we currently use check as union discriminator.

I.e., "union" types (like either, oneOf, nullOr, etc) use the provided types' check functions to check if a definition is of that type. If no permitted type matches check its throws an error, if any match, the first matching type is used.

In this way, it'd be useless to declare an either type with two types that both "check" for the same thing.

As I said before, you can work around this using lib.types.addCheck which allows you to add additional conditions to a type's check function. The NixOS manual has an example of extending a type's check and an example of overriding it.

we should do something along !merged.headError && discriminator merged.value

This is a proposal for how union types can be smarter, by taking advantage of v2 check&merge. Essentially, the v2 system was recently added to Nixpkgs and combines the checking and merging responsibility into a single function called merge.v2. The v2 interface allows definition merging to return additional metadata, such as whether merging encountered any errors.

hsjobeki is suggesting that Nixpkgs could distinguish between a union of submodules by selecting the first one that can handle the definition without errors. That's probably a more useful default behavior, although it may have a performance cost and still wouldn't cover all scenarios. E.g. some scenarios don't have a sensible solution; how to handle a module-definition that doesn't define any options? Or defines options that'd be valid in multiple submodule configurations? Or a module that declares additional options? Or how to handle freeform submodules?

builtins.unsafeGetAttrPos

:O :O :O