That looks like a feature of gradual typing: unless you exlicitly specify type annotations, it can infer type, be it ?, ? -> ? or more complicated.
But I'm too interested on how to specify type for `if` without introducing local lambda (e.g., will there be special syntax for this). 2017-03-29 19:25 GMT+03:00 Mateusz Kowalczyk <[email protected]>: > 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 >
_______________________________________________ nix-dev mailing list [email protected] http://lists.science.uu.nl/mailman/listinfo/nix-dev
