Add typing information for all builtins (revisit after #1016)

[jwiegley]

For example, builtins.add would have the type: TMany [typeInt ~> typeInt, typeInt ~> typeFloat, typeFloat ~> typeInt, typeFloat ~> typeFloat]

[johnchildren]

I'd be interested in attempting to do this, but am very much still a Haskell rookie.

Where would be the best way to add this? My naive approach would be to just add a HashMap in Nix.Types.Builtins with the information, but I'm guessing you would want to make sure that each builtin defined in Nix.Builtins has an associated type?

[jwiegley]

Yes, my inclination would be to add a Type member to the existing Builtin record, which forces every Builtin to have a type. Then, when we go to produce the attrset of builtins, we produce the HashMap you're thinking of at the same time, and make it available via some new function like baseEnv, called maybe baseTypes.

[johnchildren]

I think I will attempt to try this at the weekend then! Thank you for the pointers.

[johnchildren]

Okay, so I've started trying to do this using primops.cc as a reference, along with the nix manual, but I had a few questions about how to contribute cleanly.

I've had to use a qualified import as TSet and TList are ambiguous, with imports Nix.Value, but have temporarily used T as the qualifier, would Typing, Type or Types be better?

Next, I have extended wrap to include the type information but have ended up with an odd ordering of arguments in the where block, is there a cleaner way to express this or should I move the placement of the type information in the Builtin record.

johnchildren@7065a91

Also appreciate any other early feedback and thanks in advance, I hope I am not blocking anything!

edit: I now realise I am being foolish and can just check the implementations of each builtin as well.

[jwiegley]

How about this for a way to avoid ambiguity: We create a set of function exports from the Type module that represent all of the possible types using a consistent naming scheme:

• intT
• floatT
• setT
• listT
• etc.

Then we can just hide the Type type and its constructor to avoid ambiguity. This will also serve to make the declared types a bit more compact and readable, in my opinion. Infer.hs will need to change to match, or you can just add these aliases to what's already there and leave the rest of the code unchanged.

Other than that, you're headed in the right direction!

[johnchildren]

Okay, I like this a lot, will experiment and see what I can do!

[hSloan]

@johnchildren Hey, how's it going so far with this?

[johnchildren]

A little mixed, I wasn't able to work on it as much as I would have liked the past few weeks, but picked it up again as I am currently at ZuriHac. I initially had some trouble groking the way heterogenous lists and attribute sets should be typed, but I think I understand what I was doing wrong now. The issue is that in order to define some of the types of the builtins I may need dependent types, which may be undesirable if unavoidable?

Some examples of this are listToAttrs and attrValues which require extra type information to be unified correctly I think? I will be experimenting with this more this afternoon so will try to update with anything I find, though I feel like there might be an easier way to do this that I am missing.

edit: I suppose this is because I need the equivalent of state.forceValue to be expressed in types?

[picnoir]

I am fixing the kinda related #277 and was actually thinking about adding some type information. Did you made progress on this?

PS: I was also at ZuriHac, too bad we did not meet.

[johnchildren]

Ah that's a shame, I considered asking in the #nix channel for help but was moving between a few different rooms and didn't commit as much time to this issue as I could have.

I didn't manage to make much progress, but most builtins involve a list or set in some way so I can't see a way to type them easily. The small fruit of my efforts can be seen here. I've defined everything I am not sure about as undefined so it could potentially be merged but I have a few comments on things that need to be cleaned up.

Have been trying to read up on the way the HList package works as well as a few other concepts to see if I can find a solution, but it may take some time for me to really grok this, so would recommend that someone else pick this up if they can. I'll keep working on it anyway though.

edit: The other issue is that though I could evaluate expressions they do have side effects so I don't really want to do that just to type check for dependent types?

[johnchildren]

The other issue I encountered was typing functions that performed some kind of type inspection, for example toString, toXML or isBool. These functions could be defined with type vars but they would typically have type classes of some kind in Haskell (i.e. Show for to toString), but unfortunately we don't have access to an equivalent.

A lot of these functions will work on any possible type just due to their implementation so should be reasonably "safe", but it's not something guaranteed by the type system.

[jwiegley]

You should be able to type them with variables:

Forall [TV "a"] (TVar (TV "a") :~> typeBool)

I haven't tried this manually before, but you can use the output from --check on test functions to verify:

./dist/build/hnix/hnix --check --expr "x: if builtins.isString x then true else false"
Type of expression: [ Forall [ TV "a" ] ((:~>) (TVar (TV "a")) (TCon "boolean")) ]

Where typeBool is an alias for TCon "boolean".

[johnchildren]

Ah thanks, using --check to see is a really good idea, I'm going to try and focus on writing some automated tests for this in the coming week, but unsure of the best approach yet.

[Anton-Latukha]

--check at least from 0.6.1 release (in a year after the previous message) apparently reproducibly makes GHC throw a <<loop>> (seems like when a set is inspected), see #1016.

[jwiegley]

That often points to some unexpected let recursion.