[Nix-dev] Typing nix − funding campaign

[Théophane Hufschmitt]

Hi Mateusz,

Wed 29 Mar 17 − 17:25, Mateusz Kowalczyk(fuuzetsu at fuuzetsu.co.uk) a écrit:
> I'm sure you've answered this ad nauseum before but I wonder how you're
> going to type sets? They are bread-and-butter in nixpkgs. Presumably
> they will be typed on their fields with the standard subtyping, like
> anonymous records.

I didn't talk about records, because they are a quite difficult topic,
and I don't exactly know what their typing will look like in the end.

The problem is that the classical row-type approach (like described in
[3] for example) which is used to type anonymous records in ML-like
languages doesn't fit at all with union and intersection types.
There is an existing formalism that deals with monomorphic records in
this context (described in the chapter 9 of [1] − in french − and −
slightly more explained, but maybe less complete − in section 4.5 of
[2]).  The extension of this formalism to polymorphic records is the
current work of a Phd student (so far everything seems to works without
problem, but I don't want to talk too much about it without being sure).


> Secondly, I wonder about the motivation for the typing of `if` with
> intersections. It seems counter-intuitive to have it in the type-system.
> Why not provide an explicit union type as part of some standard library?
> I would have thought that most people expect `if` to have `Bool -> a ->
> a -> a` type. Error messages suffer because it becomes unclear whether
> the caller to `if` is expecting wrong type or the `if` is providing
> wrong type. I don't think that sort of `if` usage is common in nixpkgs
> (at least not so common to justify weird typing as opposed to just
> fixing the uses which in turn could be detected if we don't have this
> typing rule).

Were it just up to me, I would have rewritten the nix language with full
algebraic datatypes and a proper Hindley-Milner type system ;) (dhall,
I'm looking at you).
The problem with this is that it would require rewriting a large part of
nixpkgs (especially rewriting the whole nixos module system which rely
on ad-hoc polymorphism a lot), which is not possible.
That sort of usage of `if` isn't that common indeed, but it appears in
critical places (the fact that nixos modules can have different forms
for example leads to necessary typecases that couldn't be typed without
refining the type environment inside the `if`s, or the `types.either`
construct for example).
And to be honnest, with union types, you can have singleton types for
free (*ie* to each value you associate a type that contains only this
value), and the typing rules for `if`s become really nice.


Hope that answers your questions (if not, I'll be happy to explain
myself more)

-- 
Théophane Hufschmitt

[1]: http://www.diku.dk/hjemmesider/ansatte/henglein/papers/frisch2004c.pdf
[2]: https://www.irif.fr/~gc/papers/contravarianceagain.pdf
[3]: http://gallium.inria.fr/~remy/ftp/taoop1.pdf
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: <http://lists.science.uu.nl/pipermail/nix-dev/attachments/20170330/e98c84c8/attachment.sig>