[Nix-dev] Typing nix − funding campaign

[Théophane Hufschmitt]

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(simons at 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 at lists.science.uu.nl
> http://lists.science.uu.nl/mailman/listinfo/nix-dev

-- 
Théophane Hufschmitt
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: not available
URL: <http://lists.science.uu.nl/pipermail/nix-dev/attachments/20170113/df1a2594/attachment.sig>