Regarding subtying, I wonder if you're familiar with [1]. This was described to me as "the right approach to subtyping". I can't myself judge, but it does sound cool.
1. https://www.cl.cam.ac.uk/~sd601/thesis.pdf On 30 March 2017 at 08:05, Théophane Hufschmitt <rg_ni...@regnat.ovh> wrote: > Hi Mateusz, > > Wed 29 Mar 17 − 17:25, Mateusz Kowalczyk(fuuze...@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 > > _______________________________________________ > nix-dev mailing list > nix-dev@lists.science.uu.nl > http://lists.science.uu.nl/mailman/listinfo/nix-dev > >
_______________________________________________ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev