[Nix-dev] Typing nix − funding campaign

[Arseniy Alekseyev]

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_nixos at regnat.ovh> wrote:

> 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
>
> _______________________________________________
> nix-dev mailing list
> nix-dev at lists.science.uu.nl
> http://lists.science.uu.nl/mailman/listinfo/nix-dev
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.science.uu.nl/pipermail/nix-dev/attachments/20170330/1f762bbd/attachment-0001.html>