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. _______________________________________________ nix-dev mailing list [email protected] http://lists.science.uu.nl/mailman/listinfo/nix-dev
