[Nix-dev] Typing nix − funding campaign

[Mateusz Kowalczyk]

On 03/28/2017 10:45 AM, Théophane Hufschmitt wrote:
> Hi everyone,
> 
> My internship has now started, and I'll try to post regular updates on
> https://typing-nix.regnat.ovh/ as promised. So if you're interested,
> just follow the rss :)
> 
>> -- 
>> Théophane Hufschmitt
> 

Hi,

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.

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).

If stuff like this is already written somewhere, let me know and I'll RTFM.


[1]: https://typing-nix.regnat.ovh/posts/lets-type-nix.html


-- 
Mateusz K.