Hi Peter, Well... That's not exactly how things happened.
First I have to amend myself, my sentence is indeed inexact, it should have been "The inference algorithm that is *likely* going to be used is no trivial at all to implement". The story is that I first discussed with one of my teachers (Didier Remy, an OCaml core developer and expert on ML type system) about the opportunity to try typing nix. After some explanations about the language, it was clear that Hindley-Milner style type inference was clearly not possible (because of things like the presence of types at runtime and predicates such as `isInt` or `isString` which fundamentally break unification). So he asked me to think on how a type system for nix could look like, and after reflexion, I came up with something that was roughly the basis of Guiseppe Castagna's − my actual advisor − work (note that at this time I didn't know at all about his research). That's why he redirected me to him, and his works are gonna be the main axis for my work. But the goal isn't of course to try to apply it regardless of the alternatives, and that's why the first two months will be devoted for a large part to the study of the state of the art to determine the best system to use. Fri 13 Jan 17 − 10:10, Peter Simons(sim...@nospf.cryp.to) a écrit: > Hi Théophane, > > > The inference algorithm that is going to be used is no trivial at all > > to implement. > > my understanding now is that your thesis adviser has invented (or > significantly contributed to) a new type system, and the purposes of > your project is to test that particular system in practice using Nix as > a case study so that you can gain insights into the nature of that type > system and find possibilities to extend it. > > In other words, there is no way the outcome of your research will be > something like "Hindley-Milner works great for Nix and all you need is > the following minor changes to the language to allow for explicit type > annotations". That's not going to happen, because you'll never examine > whether Hindley-Milner would, in fact, be sufficient for our purposes. > > Is that a fair description of the reality? > > Best regards, > Peter > > _______________________________________________ > nix-dev mailing list > nix-dev@lists.science.uu.nl > http://lists.science.uu.nl/mailman/listinfo/nix-dev -- Théophane Hufschmitt
signature.asc
Description: PGP signature
_______________________________________________ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
