Re: [Nix-dev] Typing nix − funding campaign
Hello, Théophane Hufschmitt skribis: > 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 attribute sets are often used like records, but they are not records at all. Rather, they’re roughly hash tables where the key is a string/symbol. In Guix we use actual records where needed so that we can verify basic properties at compilation time, such as field names. Record types are disjoint from one another, which allows at least for run-time type checking. Ludo’. ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
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 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 30 Mar 17 − 00:23, Jeaye(cont...@jeaye.com) a écrit: > Congrats on the funding! Thanks :) > As someone who's been looking for more static validation of my Nix > expressions, this is an exciting change. I must admit, however, that I wonder > if Nix is just not the "right" tool for the job. I didn't see anyone else in > this thread mention it, to my surprise, so I'll bite: if you have some > funding and some time, why not integrate an existing language, with a > working, mature, static type system instead? > > This is where I think Guix made a better choice: many people already know > Scheme and are comfortable with it. If Haskell, for example, has the kind of > type system we're seeking, what benefit do we get for sticking with Nix? Only > the sunken cost? > > If it isn't clear, I think that purely functional package management is a > wonderful thing, but I don't think a new (Nix) language is the best way to > use it. I don't think a dedicated (and new) language is a bad think because nixpkgs is a quite hudge codebase (and could be much bigger) where most of the code follows exactly the same few patterns (calls to `mkDerivation` or nixos module declarations), so I think the cost of maintaining a language optimized for those patterns is worth it (for scheme, lisp users tend to think that it is flexible enough to fit as a perfect DSL for any use case, so if this is indeed true, it also is an excellent choice − I always wanted to try some lisp but never found the strenght to fight those cohorts of parens so I couldn't make my own opinion on this). And the real cost of switching to a new language would probably be − much more than the sinking cost − the unavoidable split of the community (which already isn't that big...). (And for haskell in particular − at least GHC-haskell −, I really wouldn't like it for nixpkgs because I *really* wouln't want nix to depend on something as huge as GHC). That being said, I agree that nix is somehow weird (and I agree even more after having worked a bit on the grammar), and I would have by far preferred something closer to classical functional languages. -- 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
Re: [Nix-dev] Typing nix − funding campaign
Wed 29 Mar 17 − 19:45, Danylo Hlynskyi(abcz2.upr...@gmail.com) a écrit: > 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). I'll add some type annotations of course (To be honnest, I doubt the second example could ever be typed that precisely without any annotation ; in the best case, it would probably have a type like `(bool|int) -> (string|bool)`). I don't know what the actual syntax would be (I hope I'll be able to make may case for introducing them directly into the language, if not they will be included into comments). But if your question was "what's the type of `if isInt x then x+1 else !x`, then the answer is "it depends on the type of x in the context". Depending on the type `τ` of x, it could have several types, like - If `τ` is a subtype of `int`: `int` - If `τ` is a subtype of `bool`: `bool` - If `τ` is a subtype of `int|bool`: `int|bool` (or even more precise: If `τ` is a subtype of `true`, then the `if` can be given the type `false` because `!` has type `(true -> false)&(false -> true)`) -- 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
Re: [Nix-dev] Typing nix − funding campaign
Congrats on the funding! As someone who's been looking for more static validation of my Nix expressions, this is an exciting change. I must admit, however, that I wonder if Nix is just not the "right" tool for the job. I didn't see anyone else in this thread mention it, to my surprise, so I'll bite: if you have some funding and some time, why not integrate an existing language, with a working, mature, static type system instead? This is where I think Guix made a better choice: many people already know Scheme and are comfortable with it. If Haskell, for example, has the kind of type system we're seeking, what benefit do we get for sticking with Nix? Only the sunken cost? If it isn't clear, I think that purely functional package management is a wonderful thing, but I don't think a new (Nix) language is the best way to use it. signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
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 signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
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 : > 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 > 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
Re: [Nix-dev] Typing nix − funding campaign
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 nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Could you add you blog to this list -> https://github.com/NixOS/nixos-org-configurations/blob/master/nixos-org/planet-feeds.nix (Just send a PR) Then blogs are here: http://planet.nixos.org > On 28 March 2017 at 12:05 Maarten Hoogendoorn wrote: > > > Good luck, and have fun ;) > > 2017-03-28 11:45 GMT+02:00 Théophane Hufschmitt : > > > 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 > > > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > > Hi, > > > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > > wish to start a six month length internship on giving nix a type > > > system. > > > > > > Numtide offered to fund a part of the internship, but we still need > > > some help for me to be able to start it. > > > > > > The goal of the internship is to design (and implement) a type system > > > for nix in order to be able to statically get some guaranties about > > > the well-foundness of the nixpkgs repo (or any nix expression), in > > > complement to hydra or travis tests which may let some inconsistencies > > > pass − especially on nixos module system which is way harder to test. > > > > > > Providing nix with a proper type system is a long running issue (see > > > https://github.com/NixOS/nix/issues/14), and I think a huge > > > opportunity for nix to improve its awesomeness. > > > > > > The crowdfunding campaign (and a slightly more detailled description of > > > the project) is open at https://www.gofundme.com/typing-nix, and you > > > are all invited to donate. > > > > > > Of course, I'll be happy to answer any question, by mail or on > > > irc/matrix (I am regnat[m] on freenode). > > > > > > > ___ > > 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 -- Rok Garbas, https://garbas.si ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Good luck, and have fun ;) 2017-03-28 11:45 GMT+02:00 Théophane Hufschmitt : > 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 > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > Hi, > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > wish to start a six month length internship on giving nix a type > > system. > > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > > > The goal of the internship is to design (and implement) a type system > > for nix in order to be able to statically get some guaranties about > > the well-foundness of the nixpkgs repo (or any nix expression), in > > complement to hydra or travis tests which may let some inconsistencies > > pass − especially on nixos module system which is way harder to test. > > > > Providing nix with a proper type system is a long running issue (see > > https://github.com/NixOS/nix/issues/14), and I think a huge > > opportunity for nix to improve its awesomeness. > > > > The crowdfunding campaign (and a slightly more detailled description of > > the project) is open at https://www.gofundme.com/typing-nix, and you > > are all invited to donate. > > > > Of course, I'll be happy to answer any question, by mail or on > > irc/matrix (I am regnat[m] on freenode). > > > > ___ > 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
Re: [Nix-dev] Typing nix − funding campaign
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 Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > Hi, > > I am Théophane Hufschmitt, a french master degree CS student, and I > wish to start a six month length internship on giving nix a type > system. > > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. > > The goal of the internship is to design (and implement) a type system > for nix in order to be able to statically get some guaranties about > the well-foundness of the nixpkgs repo (or any nix expression), in > complement to hydra or travis tests which may let some inconsistencies > pass − especially on nixos module system which is way harder to test. > > Providing nix with a proper type system is a long running issue (see > https://github.com/NixOS/nix/issues/14), and I think a huge > opportunity for nix to improve its awesomeness. > > The crowdfunding campaign (and a slightly more detailled description of > the project) is open at https://www.gofundme.com/typing-nix, and you > are all invited to donate. > > Of course, I'll be happy to answer any question, by mail or on > irc/matrix (I am regnat[m] on freenode). > signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
On 2017-01-12 14:13, Théophane Hufschmitt wrote: > Hi, > [--snip--] This might be of interest: http://www.haskellforall.com/2017/01/typed-nix-programming-using-dhall.html ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
People from tweag.io offered to fund the rest of the campaign, which is now complete. Thanks to all the supporters ! The internship will begin in march, and as promised, I'll send a link to a blog where I'll regularly report on my progress. Cheers everyone -- Théophane Hufschmitt Tue 17 Jan 17 − 14:04, Domen Kožar(do...@dev.si) a écrit: > Anyone who believes 500EUR/month is enough to survive in western Europe, > they should give it a shot :) > > On Tue, Jan 17, 2017 at 2:01 PM, Théophane Hufschmitt > wrote: > > > Hi everyone, > > > > Jonas told me that some people didn't understand the raise of the goal > > − it looked like "Hey, I can make money with this ! let's try to make > > even more !". I just want to clarify things a bit : > > > > The first goal was the strict legal minimum that I needed to get for > > the internship to be accepted. Now the fact is that this remains rather > > low (554.40€/month exactly), and clearly not enough to permit a comfortable > > living (I plan to take the necessary from my savings if needed, but > > that's just a safeguard and is clearly not optimal). So that's why I > > raised the goal. I apologize if felt roguish to some, there was no bad > > intention in it. > > > > Just to avoid miscomprehensions ;) > > > > -- > > Théophane Hufschmitt > > > > Sun 15 Jan 17 − 09:31, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > > Thanks everyone, this is amazing (and went amazingly fast !) > > > > > > I'll raise the goal − as I said, this goal was just the legal minimum > > > for me to be allowed to do it, but don't worry, I'll do it regardless of > > > how the rest of the campaign goes. > > > > > > So don't stop advertising this ;) > > > > > > -- > > > Théophane Hufschmitt > > > > > > Sat 14 Jan 17 − 22:23, zimbatm(zimb...@zimbatm.com) a écrit: > > > > Thanks everyone! I'm impressed by how fast that went. > > > > > > > > On Sat, 14 Jan 2017 at 20:27 Domen Kožar wrote: > > > > > > > > > It's funded :) Congratz! > > > > > > > > > > On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt < > > > > > rg_ni...@regnat.ovh> wrote: > > > > > > > > > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a > > écrit: > > > > > > Hi, > > > > > > > > > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > > > > > wish to start a six month length internship on giving nix a type > > > > > > system. > > > > > > > > > > > > Numtide offered to fund a part of the internship, but we still need > > > > > > some help for me to be able to start it. > > > > > > > > > > > > The goal of the internship is to design (and implement) a type > > system > > > > > > for nix in order to be able to statically get some guaranties about > > > > > > the well-foundness of the nixpkgs repo (or any nix expression), in > > > > > > complement to hydra or travis tests which may let some > > inconsistencies > > > > > > pass − especially on nixos module system which is way harder to > > test. > > > > > > > > > > > > Providing nix with a proper type system is a long running issue > > (see > > > > > > https://github.com/NixOS/nix/issues/14), and I think a huge > > > > > > opportunity for nix to improve its awesomeness. > > > > > > > > > > > > The crowdfunding campaign (and a slightly more detailled > > description of > > > > > > the project) is open at https://www.gofundme.com/typing-nix, and > > you > > > > > > are all invited to donate. > > > > > > > > > > > > Of course, I'll be happy to answer any question, by mail or on > > > > > > irc/matrix (I am regnat[m] on freenode). > > > > > > > > > > > > -- > > > > > > Théophane Hufschmitt > > > > > > > > > > Already one half of the required funding has been reached in less > > than > > > > > one day. A big thanks to all the donators ! > > > > > > > > > > For everyone else, there is still at lot of place if you want to be a > > > > > part of this, so don't hesitate ;) > > > > > > > > > > -- > > > > > Théophane Hufschmitt > > > > > > > > > > ___ > > > > > 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 > > > > > > > > > > > signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Anyone who believes 500EUR/month is enough to survive in western Europe, they should give it a shot :) On Tue, Jan 17, 2017 at 2:01 PM, Théophane Hufschmitt wrote: > Hi everyone, > > Jonas told me that some people didn't understand the raise of the goal > − it looked like "Hey, I can make money with this ! let's try to make > even more !". I just want to clarify things a bit : > > The first goal was the strict legal minimum that I needed to get for > the internship to be accepted. Now the fact is that this remains rather > low (554.40€/month exactly), and clearly not enough to permit a comfortable > living (I plan to take the necessary from my savings if needed, but > that's just a safeguard and is clearly not optimal). So that's why I > raised the goal. I apologize if felt roguish to some, there was no bad > intention in it. > > Just to avoid miscomprehensions ;) > > -- > Théophane Hufschmitt > > Sun 15 Jan 17 − 09:31, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > Thanks everyone, this is amazing (and went amazingly fast !) > > > > I'll raise the goal − as I said, this goal was just the legal minimum > > for me to be allowed to do it, but don't worry, I'll do it regardless of > > how the rest of the campaign goes. > > > > So don't stop advertising this ;) > > > > -- > > Théophane Hufschmitt > > > > Sat 14 Jan 17 − 22:23, zimbatm(zimb...@zimbatm.com) a écrit: > > > Thanks everyone! I'm impressed by how fast that went. > > > > > > On Sat, 14 Jan 2017 at 20:27 Domen Kožar wrote: > > > > > > > It's funded :) Congratz! > > > > > > > > On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt < > > > > rg_ni...@regnat.ovh> wrote: > > > > > > > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a > écrit: > > > > > Hi, > > > > > > > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > > > > wish to start a six month length internship on giving nix a type > > > > > system. > > > > > > > > > > Numtide offered to fund a part of the internship, but we still need > > > > > some help for me to be able to start it. > > > > > > > > > > The goal of the internship is to design (and implement) a type > system > > > > > for nix in order to be able to statically get some guaranties about > > > > > the well-foundness of the nixpkgs repo (or any nix expression), in > > > > > complement to hydra or travis tests which may let some > inconsistencies > > > > > pass − especially on nixos module system which is way harder to > test. > > > > > > > > > > Providing nix with a proper type system is a long running issue > (see > > > > > https://github.com/NixOS/nix/issues/14), and I think a huge > > > > > opportunity for nix to improve its awesomeness. > > > > > > > > > > The crowdfunding campaign (and a slightly more detailled > description of > > > > > the project) is open at https://www.gofundme.com/typing-nix, and > you > > > > > are all invited to donate. > > > > > > > > > > Of course, I'll be happy to answer any question, by mail or on > > > > > irc/matrix (I am regnat[m] on freenode). > > > > > > > > > > -- > > > > > Théophane Hufschmitt > > > > > > > > Already one half of the required funding has been reached in less > than > > > > one day. A big thanks to all the donators ! > > > > > > > > For everyone else, there is still at lot of place if you want to be a > > > > part of this, so don't hesitate ;) > > > > > > > > -- > > > > Théophane Hufschmitt > > > > > > > > ___ > > > > 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 > > > > > > > ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
2017-01-12 16:51 GMT+03:00 Marc Weber : > Have you never debugged a "got x but y expected" problem? The typesystem > is there, its just lazy as nix is - typed on evaluation. This is nothing. Haskell is typed on evaluation too. Nix is an interpreter, not a compiler :) ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi everyone, Jonas told me that some people didn't understand the raise of the goal − it looked like "Hey, I can make money with this ! let's try to make even more !". I just want to clarify things a bit : The first goal was the strict legal minimum that I needed to get for the internship to be accepted. Now the fact is that this remains rather low (554.40€/month exactly), and clearly not enough to permit a comfortable living (I plan to take the necessary from my savings if needed, but that's just a safeguard and is clearly not optimal). So that's why I raised the goal. I apologize if felt roguish to some, there was no bad intention in it. Just to avoid miscomprehensions ;) -- Théophane Hufschmitt Sun 15 Jan 17 − 09:31, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > Thanks everyone, this is amazing (and went amazingly fast !) > > I'll raise the goal − as I said, this goal was just the legal minimum > for me to be allowed to do it, but don't worry, I'll do it regardless of > how the rest of the campaign goes. > > So don't stop advertising this ;) > > -- > Théophane Hufschmitt > > Sat 14 Jan 17 − 22:23, zimbatm(zimb...@zimbatm.com) a écrit: > > Thanks everyone! I'm impressed by how fast that went. > > > > On Sat, 14 Jan 2017 at 20:27 Domen Kožar wrote: > > > > > It's funded :) Congratz! > > > > > > On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt < > > > rg_ni...@regnat.ovh> wrote: > > > > > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > > > Hi, > > > > > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > > > wish to start a six month length internship on giving nix a type > > > > system. > > > > > > > > Numtide offered to fund a part of the internship, but we still need > > > > some help for me to be able to start it. > > > > > > > > The goal of the internship is to design (and implement) a type system > > > > for nix in order to be able to statically get some guaranties about > > > > the well-foundness of the nixpkgs repo (or any nix expression), in > > > > complement to hydra or travis tests which may let some inconsistencies > > > > pass − especially on nixos module system which is way harder to test. > > > > > > > > Providing nix with a proper type system is a long running issue (see > > > > https://github.com/NixOS/nix/issues/14), and I think a huge > > > > opportunity for nix to improve its awesomeness. > > > > > > > > The crowdfunding campaign (and a slightly more detailled description of > > > > the project) is open at https://www.gofundme.com/typing-nix, and you > > > > are all invited to donate. > > > > > > > > Of course, I'll be happy to answer any question, by mail or on > > > > irc/matrix (I am regnat[m] on freenode). > > > > > > > > -- > > > > Théophane Hufschmitt > > > > > > Already one half of the required funding has been reached in less than > > > one day. A big thanks to all the donators ! > > > > > > For everyone else, there is still at lot of place if you want to be a > > > part of this, so don't hesitate ;) > > > > > > -- > > > Théophane Hufschmitt > > > > > > ___ > > > 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 > > > signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
On 01/15/2017 09:31 AM, Théophane Hufschmitt wrote: > as I said, this goal was just the legal minimum > for me to be allowed to do it That's interesting. Here in CZ it's typical that students earn absolutely nothing for their work on Bachelor and Master theses. (No offense or envy meant.) Good luck with the project! The funding *was* amazingly fast. --Vladimir smime.p7s Description: S/MIME Cryptographic Signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Thanks everyone, this is amazing (and went amazingly fast !) I'll raise the goal − as I said, this goal was just the legal minimum for me to be allowed to do it, but don't worry, I'll do it regardless of how the rest of the campaign goes. So don't stop advertising this ;) -- Théophane Hufschmitt Sat 14 Jan 17 − 22:23, zimbatm(zimb...@zimbatm.com) a écrit: > Thanks everyone! I'm impressed by how fast that went. > > On Sat, 14 Jan 2017 at 20:27 Domen Kožar wrote: > > > It's funded :) Congratz! > > > > On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt < > > rg_ni...@regnat.ovh> wrote: > > > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > > Hi, > > > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > > wish to start a six month length internship on giving nix a type > > > system. > > > > > > Numtide offered to fund a part of the internship, but we still need > > > some help for me to be able to start it. > > > > > > The goal of the internship is to design (and implement) a type system > > > for nix in order to be able to statically get some guaranties about > > > the well-foundness of the nixpkgs repo (or any nix expression), in > > > complement to hydra or travis tests which may let some inconsistencies > > > pass − especially on nixos module system which is way harder to test. > > > > > > Providing nix with a proper type system is a long running issue (see > > > https://github.com/NixOS/nix/issues/14), and I think a huge > > > opportunity for nix to improve its awesomeness. > > > > > > The crowdfunding campaign (and a slightly more detailled description of > > > the project) is open at https://www.gofundme.com/typing-nix, and you > > > are all invited to donate. > > > > > > Of course, I'll be happy to answer any question, by mail or on > > > irc/matrix (I am regnat[m] on freenode). > > > > > > -- > > > Théophane Hufschmitt > > > > Already one half of the required funding has been reached in less than > > one day. A big thanks to all the donators ! > > > > For everyone else, there is still at lot of place if you want to be a > > part of this, so don't hesitate ;) > > > > -- > > Théophane Hufschmitt > > > > ___ > > 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 > > signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Thanks everyone! I'm impressed by how fast that went. On Sat, 14 Jan 2017 at 20:27 Domen Kožar wrote: > It's funded :) Congratz! > > On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt < > rg_ni...@regnat.ovh> wrote: > > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > Hi, > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > wish to start a six month length internship on giving nix a type > > system. > > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > > > The goal of the internship is to design (and implement) a type system > > for nix in order to be able to statically get some guaranties about > > the well-foundness of the nixpkgs repo (or any nix expression), in > > complement to hydra or travis tests which may let some inconsistencies > > pass − especially on nixos module system which is way harder to test. > > > > Providing nix with a proper type system is a long running issue (see > > https://github.com/NixOS/nix/issues/14), and I think a huge > > opportunity for nix to improve its awesomeness. > > > > The crowdfunding campaign (and a slightly more detailled description of > > the project) is open at https://www.gofundme.com/typing-nix, and you > > are all invited to donate. > > > > Of course, I'll be happy to answer any question, by mail or on > > irc/matrix (I am regnat[m] on freenode). > > > > -- > > Théophane Hufschmitt > > Already one half of the required funding has been reached in less than > one day. A big thanks to all the donators ! > > For everyone else, there is still at lot of place if you want to be a > part of this, so don't hesitate ;) > > -- > Théophane Hufschmitt > > ___ > 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 > ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
It's funded :) Congratz! On Fri, Jan 13, 2017 at 10:56 AM, Théophane Hufschmitt wrote: > Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > > Hi, > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > wish to start a six month length internship on giving nix a type > > system. > > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > > > The goal of the internship is to design (and implement) a type system > > for nix in order to be able to statically get some guaranties about > > the well-foundness of the nixpkgs repo (or any nix expression), in > > complement to hydra or travis tests which may let some inconsistencies > > pass − especially on nixos module system which is way harder to test. > > > > Providing nix with a proper type system is a long running issue (see > > https://github.com/NixOS/nix/issues/14), and I think a huge > > opportunity for nix to improve its awesomeness. > > > > The crowdfunding campaign (and a slightly more detailled description of > > the project) is open at https://www.gofundme.com/typing-nix, and you > > are all invited to donate. > > > > Of course, I'll be happy to answer any question, by mail or on > > irc/matrix (I am regnat[m] on freenode). > > > > -- > > Théophane Hufschmitt > > Already one half of the required funding has been reached in less than > one day. A big thanks to all the donators ! > > For everyone else, there is still at lot of place if you want to be a > part of this, so don't hesitate ;) > > -- > Théophane Hufschmitt > > ___ > 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 14:13, Théophane Hufschmitt(rg_ni...@regnat.ovh) a écrit: > Hi, > > I am Théophane Hufschmitt, a french master degree CS student, and I > wish to start a six month length internship on giving nix a type > system. > > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. > > The goal of the internship is to design (and implement) a type system > for nix in order to be able to statically get some guaranties about > the well-foundness of the nixpkgs repo (or any nix expression), in > complement to hydra or travis tests which may let some inconsistencies > pass − especially on nixos module system which is way harder to test. > > Providing nix with a proper type system is a long running issue (see > https://github.com/NixOS/nix/issues/14), and I think a huge > opportunity for nix to improve its awesomeness. > > The crowdfunding campaign (and a slightly more detailled description of > the project) is open at https://www.gofundme.com/typing-nix, and you > are all invited to donate. > > Of course, I'll be happy to answer any question, by mail or on > irc/matrix (I am regnat[m] on freenode). > > -- > Théophane Hufschmitt Already one half of the required funding has been reached in less than one day. A big thanks to all the donators ! For everyone else, there is still at lot of place if you want to be a part of this, so don't hesitate ;) -- 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
Re: [Nix-dev] Typing nix − funding campaign
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
Re: [Nix-dev] Typing nix − funding campaign
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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 21:18, Thomas Hunger(tehun...@gmail.com) a écrit: > Hi, > > For my own curiosity: Is your adviser's work online somewhere? > Hi, All its publications are on his personal page at https://www.irif.fr/~gc/ The current work is yet unreleased, but there is a demo of some possible things at http://www.cduce.org/ocaml/bi -- 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
Re: [Nix-dev] Typing nix − funding campaign
Hi Maarten, I plan to rely heavily on Eelco's thesis for rewriting the spécifications, but it will need a serious update because of the changes that happened to the language. Integration into an ide is a long term goal, but this is probably not gonna happen anytime soon. (but using types to enhance documentation is of course planned) Le 12 janvier 2017 15:50:18 UTC+01:00, Maarten Hoogendoorn a écrit : >Interesting idea. > >Note that Eelco's phd thesis about nix contains a formal definition of >both >the syntax and semantics the language. >The whole thesis is well written and approachable. > >Potential other benefits from a deeper analysis could include: >- generation of better documentation for helper functions >- or even IDE features like jump to definition > > >2017-01-12 14:13 GMT+01:00 Théophane Hufschmitt : > >> Hi, >> >> I am Théophane Hufschmitt, a french master degree CS student, and I >> wish to start a six month length internship on giving nix a type >> system. >> >> Numtide offered to fund a part of the internship, but we still need >> some help for me to be able to start it. >> >> The goal of the internship is to design (and implement) a type system >> for nix in order to be able to statically get some guaranties about >> the well-foundness of the nixpkgs repo (or any nix expression), in >> complement to hydra or travis tests which may let some >inconsistencies >> pass − especially on nixos module system which is way harder to test. >> >> Providing nix with a proper type system is a long running issue (see >> https://github.com/NixOS/nix/issues/14), and I think a huge >> opportunity for nix to improve its awesomeness. >> >> The crowdfunding campaign (and a slightly more detailled description >of >> the project) is open at https://www.gofundme.com/typing-nix, and you >> are all invited to donate. >> >> Of course, I'll be happy to answer any question, by mail or on >> irc/matrix (I am regnat[m] on freenode). >> >> -- >> Théophane Hufschmitt >> >> ___ >> 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 15:31, Peter Simons(sim...@nospf.cryp.to) a écrit: > Hi Théophane, > > > https://www.gofundme.com/typing-nix > > I see that you plan to spend approx. 2 months (a third of the entire > project's time) on developing a parser for Nix. Why do you feel that > this is necessary, considering that there is a parser for Nix already? > > The notion of working with a separate implementation worries me because > I see the danger that your efforts are going to exist in a parallel > universe which won't be possible to merge back into Nix proper. > > Or, to put it differently, does your project even have the goal of > providing a working implementation for Nix? Or is it more about > exploring the design space for type systems that Nix could potentially > use? > > Best regards, > Peter Hi Peter, The two months are not just for formalizing the syntax and writing the parser, but also (and mostly) for bibliography. I agree with your concerns about the separate implementation. The reason for this is related to your third paragraph. The inference algorithm that is going to be used is no trivial at all to implement, and my advisor already has done a lot of work on this that could be reused, but written in OCaml, and we agreed that writing and maintaining a parser it was far easier than reimplementing what he already had done, and that it would be too hard to ship a usable product in a few month without using it. Regarding the goal of the project, it will be focused on providing a working implementation for nix (although that will of course first require exploring the possibilities for a type system for nix). There is enough theorical work to come up with something usable (and useful) for a langaige such as nix. -- Théophane Hufschmitt ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi, For my own curiosity: Is your adviser's work online somewhere? ~ On 12 January 2017 at 17:17, Théophane Hufschmitt wrote: > Thu 12 Jan 17 − 15:31, Peter Simons(sim...@nospf.cryp.to) a écrit: > > Hi Théophane, > > > > > https://www.gofundme.com/typing-nix > > > > I see that you plan to spend approx. 2 months (a third of the entire > > project's time) on developing a parser for Nix. Why do you feel that > > this is necessary, considering that there is a parser for Nix already? > > > > The notion of working with a separate implementation worries me because > > I see the danger that your efforts are going to exist in a parallel > > universe which won't be possible to merge back into Nix proper. > > > > Or, to put it differently, does your project even have the goal of > > providing a working implementation for Nix? Or is it more about > > exploring the design space for type systems that Nix could potentially > > use? > > > > Best regards, > > Peter > > Hi Peter, > > The two months are not just for formalizing the syntax and writing the > parser, but also (and mostly) for bibliography. > > I agree with your concerns about the separate implementation. > The reason for this is related to your third paragraph. The inference > algorithm that is going to be used is no trivial at all to implement, > and my advisor already has done a lot of work on this that could be > reused, but written in OCaml, and we agreed that writing and > maintaining a parser it was far easier than reimplementing what he > already had done, and that it would be too hard to ship a usable > product in a few month without using it. > > Regarding the goal of the project, it will be focused on providing a > working implementation for nix (although that will of course first > require exploring the possibilities for a type system for nix). There > is enough theorical work to come up with something usable (and useful) > for a langaige such as nix. > > -- > Théophane Hufschmitt > > Thu 12 Jan 17 − 15:31, Peter Simons(sim...@nospf.cryp.to) a écrit: > > Hi Théophane, > > > > > https://www.gofundme.com/typing-nix > > > > I see that you plan to spend approx. 2 months (a third of the entire > > project's time) on developing a parser for Nix. Why do you feel that > > this is necessary, considering that there is a parser for Nix already? > > > > The notion of working with a separate implementation worries me because > > I see the danger that your efforts are going to exist in a parallel > > universe which won't be possible to merge back into Nix proper. > > > > Or, to put it differently, does your project even have the goal of > > providing a working implementation for Nix? Or is it more about > > exploring the design space for type systems that Nix could potentially > > use? > > > > Best regards, > > Peter > > Hi Peter, > > The two months are not just for formalizing the syntax and writing the > parser, but also (and mostly) for bibliography. > > I agree with your concerns about the separate implementation. > The reason for this is related to your third paragraph. The inference > algorithm that is going to be used is no trivial at all to implement, > and my advisor already has done a lot of work on this that could be > reused, but written in OCaml, and we agreed that writing and > maintaining a parser it was far easier than reimplementing what he > already had done, and that it would be too hard to ship a usable > product in a few month without using it. > > Regarding the goal of the project, it will be focused on providing a > working implementation for nix (although that will of course first > require exploring the possibilities for a type system for nix). There > is enough theorical work to come up with something usable (and useful) > for a langaige such as nix. > > -- > Théophane Hufschmitt > > ___ > 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 18:30, Michael Raskin(7c6f4...@mail.ru) a écrit: > >I agree with your concerns about the separate implementation. > >The reason for this is related to your third paragraph. The inference > >algorithm that is going to be used is no trivial at all to implement, > >and my advisor already has done a lot of work on this that could be > >reused, but written in OCaml, and we agreed that writing and > >maintaining a parser it was far easier than reimplementing what he > >already had done, and that it would be too hard to ship a usable > >product in a few month without using it. > > Have you considered making nix-instantiate --parse-only work with --xml > like --eval-only does? May reduce the total effort needed (if it turns > out to be reasonably simple) I haven't, but it is worth considerating, indeed (but I fear that it would require some modifications to the nix parser in order to be useful for me). If nothing more, this could be a good way to test my parser against the official one. -- Théophane Hufschmitt ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 19:36, Profpatsch(m...@profpatsch.de) a écrit: > On 17-01-12 07:31pm, Théophane Hufschmitt wrote: > > I'd want to support exactly the same syntax as nix does. That would > > mean (depending of the position of the nix core-dev team about this) > > either that the nix syntax would be extended to support type > > annotations, either that those would be included in comments. > > If you want to write a nix parser, you can take a look at > https://hackage.haskell.org/package/hnix > > Also, Gabriel took a quick shot at one, but it’s unfinished: > https://github.com/Gabriel439/nixfmt > > Hope it works for you, writing parsers is tricky. Especially the > string splicing in nixexprs. > > -- > Proudly written in Mutt with Vim on NixOS. > Q: Why is this email five sentences or less? > A: http://five.sentenc.es > May take up to five days to read your message. If it’s urgent, call me. I'd heard about hnix, but didn't know nixfmt. I'll keep them as references for when I actually write the parser -- 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 15:13, Profpatsch(m...@profpatsch.de) a écrit: > On 17-01-12 02:13pm, Théophane Hufschmitt wrote: > > type system for nix > > I’m excited. > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > If GsoC can be made to work, maybe the $5000 (or something like that) > can be added? Not sure if that is allowed from the GsoC rules though. > > > -- > Proudly written in Mutt with Vim on NixOS. > Q: Why is this email five sentences or less? > A: http://five.sentenc.es > May take up to five days to read your message. If it’s urgent, call me. If it can work that would be awesome. I'll look further into this tomorrw, thanks for the advice -- 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
Re: [Nix-dev] Typing nix − funding campaign
On 17-01-12 07:31pm, Théophane Hufschmitt wrote: > I'd want to support exactly the same syntax as nix does. That would > mean (depending of the position of the nix core-dev team about this) > either that the nix syntax would be extended to support type > annotations, either that those would be included in comments. If you want to write a nix parser, you can take a look at https://hackage.haskell.org/package/hnix Also, Gabriel took a quick shot at one, but it’s unfinished: https://github.com/Gabriel439/nixfmt Hope it works for you, writing parsers is tricky. Especially the string splicing in nixexprs. -- Proudly written in Mutt with Vim on NixOS. Q: Why is this email five sentences or less? A: http://five.sentenc.es May take up to five days to read your message. If it’s urgent, call me. signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi Thomas, Thanks for the donation :) I don't plan to try making this builtin into the nix codebase (at least not for now) for several reasons, essentially : - As I explained to Peter, the code will be in OCaml, so it won't be mergeable at all. - The tool will probably only be useful for nix developpers, and it makes sense to me that it is not shipped with nix, as it won't be of any use to the casual user. - This would be a huge modification for nix, so it won't be worth merging anyway until the tool is polished enough (so not before the end of the internship). I'd want to support exactly the same syntax as nix does. That would mean (depending of the position of the nix core-dev team about this) either that the nix syntax would be extended to support type annotations, either that those would be included in comments. Thu 12 Jan 17 − 14:33, Thomas Hunger(tehun...@gmail.com) a écrit: > Hi, > > Many thanks for giving this a shot, it's exciting! I donated some money and > I hope we'll get this rolling soon. > > I have a few questions: > > * Is the plan to merge this into the current nix c++ code base? If so: Do > you have some buy-in from the nix maintainers? > * If it's an external tool: would it compile to untyped nix, like e.g. flow > and TypeScript do? > > ~ > > > > On 12 January 2017 at 13:13, Théophane Hufschmitt > wrote: > > > Hi, > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > wish to start a six month length internship on giving nix a type > > system. > > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > > > The goal of the internship is to design (and implement) a type system > > for nix in order to be able to statically get some guaranties about > > the well-foundness of the nixpkgs repo (or any nix expression), in > > complement to hydra or travis tests which may let some inconsistencies > > pass − especially on nixos module system which is way harder to test. > > > > Providing nix with a proper type system is a long running issue (see > > https://github.com/NixOS/nix/issues/14), and I think a huge > > opportunity for nix to improve its awesomeness. > > > > The crowdfunding campaign (and a slightly more detailled description of > > the project) is open at https://www.gofundme.com/typing-nix, and you > > are all invited to donate. > > > > Of course, I'll be happy to answer any question, by mail or on > > irc/matrix (I am regnat[m] on freenode). > > > > -- > > Théophane Hufschmitt > > > > ___ > > 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
Re: [Nix-dev] Typing nix − funding campaign
Thu 12 Jan 17 − 15:31, Peter Simons(sim...@nospf.cryp.to) a écrit: > Hi Théophane, > > > https://www.gofundme.com/typing-nix > > I see that you plan to spend approx. 2 months (a third of the entire > project's time) on developing a parser for Nix. Why do you feel that > this is necessary, considering that there is a parser for Nix already? > > The notion of working with a separate implementation worries me because > I see the danger that your efforts are going to exist in a parallel > universe which won't be possible to merge back into Nix proper. > > Or, to put it differently, does your project even have the goal of > providing a working implementation for Nix? Or is it more about > exploring the design space for type systems that Nix could potentially > use? > > Best regards, > Peter Hi Peter, The two months are not just for formalizing the syntax and writing the parser, but also (and mostly) for bibliography. I agree with your concerns about the separate implementation. The reason for this is related to your third paragraph. The inference algorithm that is going to be used is no trivial at all to implement, and my advisor already has done a lot of work on this that could be reused, but written in OCaml, and we agreed that writing and maintaining a parser it was far easier than reimplementing what he already had done, and that it would be too hard to ship a usable product in a few month without using it. Regarding the goal of the project, it will be focused on providing a working implementation for nix (although that will of course first require exploring the possibilities for a type system for nix). There is enough theorical work to come up with something usable (and useful) for a langaige such as nix. -- Théophane Hufschmitt Thu 12 Jan 17 − 15:31, Peter Simons(sim...@nospf.cryp.to) a écrit: > Hi Théophane, > > > https://www.gofundme.com/typing-nix > > I see that you plan to spend approx. 2 months (a third of the entire > project's time) on developing a parser for Nix. Why do you feel that > this is necessary, considering that there is a parser for Nix already? > > The notion of working with a separate implementation worries me because > I see the danger that your efforts are going to exist in a parallel > universe which won't be possible to merge back into Nix proper. > > Or, to put it differently, does your project even have the goal of > providing a working implementation for Nix? Or is it more about > exploring the design space for type systems that Nix could potentially > use? > > Best regards, > Peter Hi Peter, The two months are not just for formalizing the syntax and writing the parser, but also (and mostly) for bibliography. I agree with your concerns about the separate implementation. The reason for this is related to your third paragraph. The inference algorithm that is going to be used is no trivial at all to implement, and my advisor already has done a lot of work on this that could be reused, but written in OCaml, and we agreed that writing and maintaining a parser it was far easier than reimplementing what he already had done, and that it would be too hard to ship a usable product in a few month without using it. Regarding the goal of the project, it will be focused on providing a working implementation for nix (although that will of course first require exploring the possibilities for a type system for nix). There is enough theorical work to come up with something usable (and useful) for a langaige such as nix. -- Théophane Hufschmitt ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi Maarten, I plan to rely heavily on Eelco's thesis for rewriting the spécifications, but it will need a serious update because of the changes that happened to the language. Integration into an ide is a long term goal, but this is probably not gonna happen anytime soon. (but using types to enhance documentation is of course planned) Le 12 janvier 2017 15:50:18 UTC+01:00, Maarten Hoogendoorn a écrit : >Interesting idea. > >Note that Eelco's phd thesis about nix contains a formal definition of >both >the syntax and semantics the language. >The whole thesis is well written and approachable. > >Potential other benefits from a deeper analysis could include: >- generation of better documentation for helper functions >- or even IDE features like jump to definition > > >2017-01-12 14:13 GMT+01:00 Théophane Hufschmitt : > >> Hi, >> >> I am Théophane Hufschmitt, a french master degree CS student, and I >> wish to start a six month length internship on giving nix a type >> system. >> >> Numtide offered to fund a part of the internship, but we still need >> some help for me to be able to start it. >> >> The goal of the internship is to design (and implement) a type system >> for nix in order to be able to statically get some guaranties about >> the well-foundness of the nixpkgs repo (or any nix expression), in >> complement to hydra or travis tests which may let some >inconsistencies >> pass − especially on nixos module system which is way harder to test. >> >> Providing nix with a proper type system is a long running issue (see >> https://github.com/NixOS/nix/issues/14), and I think a huge >> opportunity for nix to improve its awesomeness. >> >> The crowdfunding campaign (and a slightly more detailled description >of >> the project) is open at https://www.gofundme.com/typing-nix, and you >> are all invited to donate. >> >> Of course, I'll be happy to answer any question, by mail or on >> irc/matrix (I am regnat[m] on freenode). >> >> -- >> Théophane Hufschmitt >> >> ___ >> nix-dev mailing list >> nix-dev@lists.science.uu.nl >> http://lists.science.uu.nl/mailman/listinfo/nix-dev >> >> Hi Maarten, I plan to rely heavily on Eelco's thesis for rewriting the spécifications, but it will need a serious update because of the changes that happened to the language. Integration into an ide is a long term goal, but this is probably not gonna happen anytime soon. (but using types to enhance documentation is of course planned) Le 12 janvier 2017 15:50:18 UTC+01:00, Maarten Hoogendoorn a écrit : >Interesting idea. > >Note that Eelco's phd thesis about nix contains a formal definition of >both >the syntax and semantics the language. >The whole thesis is well written and approachable. > >Potential other benefits from a deeper analysis could include: >- generation of better documentation for helper functions >- or even IDE features like jump to definition > > >2017-01-12 14:13 GMT+01:00 Théophane Hufschmitt : > >> Hi, >> >> I am Théophane Hufschmitt, a french master degree CS student, and I >> wish to start a six month length internship on giving nix a type >> system. >> >> Numtide offered to fund a part of the internship, but we still need >> some help for me to be able to start it. >> >> The goal of the internship is to design (and implement) a type system >> for nix in order to be able to statically get some guaranties about >> the well-foundness of the nixpkgs repo (or any nix _expression_), in >> complement to hydra or travis tests which may let some >inconsistencies >> pass − especially on nixos module system which is way harder to test. >> >> Providing nix with a proper type system is a long running issue (see >> https://github.com/NixOS/nix/issues/14), and I think a huge >> opportunity for nix to improve its awesomeness. >> >> The crowdfunding campaign (and a slightly more detailled description >of >> the project) is open at https://www.gofundme.com/typing-nix, and you >> are all invited to donate. >> >> Of course, I'll be happy to answer any question, by mail or on >> irc/matrix (I am regnat[m] on freenode). >> >> -- >> Théophane Hufschmitt >> >> ___ >> 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
Re: [Nix-dev] Typing nix − funding campaign
>Note that Eelco's phd thesis about nix contains a formal definition of both >the syntax and semantics the language. But remember that it contains a formal definition of the language at the moment when the thesis has been written (obviously), and the current state of NixPkgs and NixOS relies on some significant changes that have been made since then. ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Interesting idea. Note that Eelco's phd thesis about nix contains a formal definition of both the syntax and semantics the language. The whole thesis is well written and approachable. Potential other benefits from a deeper analysis could include: - generation of better documentation for helper functions - or even IDE features like jump to definition 2017-01-12 14:13 GMT+01:00 Théophane Hufschmitt : > Hi, > > I am Théophane Hufschmitt, a french master degree CS student, and I > wish to start a six month length internship on giving nix a type > system. > > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. > > The goal of the internship is to design (and implement) a type system > for nix in order to be able to statically get some guaranties about > the well-foundness of the nixpkgs repo (or any nix expression), in > complement to hydra or travis tests which may let some inconsistencies > pass − especially on nixos module system which is way harder to test. > > Providing nix with a proper type system is a long running issue (see > https://github.com/NixOS/nix/issues/14), and I think a huge > opportunity for nix to improve its awesomeness. > > The crowdfunding campaign (and a slightly more detailled description of > the project) is open at https://www.gofundme.com/typing-nix, and you > are all invited to donate. > > Of course, I'll be happy to answer any question, by mail or on > irc/matrix (I am regnat[m] on freenode). > > -- > Théophane Hufschmitt > > ___ > 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
Re: [Nix-dev] Typing nix − funding campaign
Hi, Many thanks for giving this a shot, it's exciting! I donated some money and I hope we'll get this rolling soon. I have a few questions: * Is the plan to merge this into the current nix c++ code base? If so: Do you have some buy-in from the nix maintainers? * If it's an external tool: would it compile to untyped nix, like e.g. flow and TypeScript do? ~ On 12 January 2017 at 13:13, Théophane Hufschmitt wrote: > Hi, > > I am Théophane Hufschmitt, a french master degree CS student, and I > wish to start a six month length internship on giving nix a type > system. > > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. > > The goal of the internship is to design (and implement) a type system > for nix in order to be able to statically get some guaranties about > the well-foundness of the nixpkgs repo (or any nix expression), in > complement to hydra or travis tests which may let some inconsistencies > pass − especially on nixos module system which is way harder to test. > > Providing nix with a proper type system is a long running issue (see > https://github.com/NixOS/nix/issues/14), and I think a huge > opportunity for nix to improve its awesomeness. > > The crowdfunding campaign (and a slightly more detailled description of > the project) is open at https://www.gofundme.com/typing-nix, and you > are all invited to donate. > > Of course, I'll be happy to answer any question, by mail or on > irc/matrix (I am regnat[m] on freenode). > > -- > Théophane Hufschmitt > > ___ > 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
Re: [Nix-dev] Typing nix − funding campaign
Hi Théophane, > https://www.gofundme.com/typing-nix I see that you plan to spend approx. 2 months (a third of the entire project's time) on developing a parser for Nix. Why do you feel that this is necessary, considering that there is a parser for Nix already? The notion of working with a separate implementation worries me because I see the danger that your efforts are going to exist in a parallel universe which won't be possible to merge back into Nix proper. Or, to put it differently, does your project even have the goal of providing a working implementation for Nix? Or is it more about exploring the design space for type systems that Nix could potentially use? Best regards, Peter ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
> What about guix https://www.gnu.org/software/guix/ ? > Does some typing exist here already? There exist things (which are among the stuff I plan to study before designing the system) for scheme (like http://www.ccs.neu.edu/racket/pubs/popl08-thf.pdf), but as far as I know, nothing special to guile (and hence to guix). > If you need a nice idea about "how to improve the world" - nix guix and > the JS implemenation (and the 100+ other distros) clearly say that a > cross platform cross language package manage / depndency system is > required to derive .nix / guix /whatsoever packages from .. > > It should allow "platforms" (like Haskell) to have "stable bases" to > work on. > > That would be awesome and the whole open source community & nix would > benefit IMHO. That's slightly out of topic, but why wouldn't the drv system work for this -- 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
Re: [Nix-dev] Typing nix − funding campaign
On 17-01-12 02:13pm, Théophane Hufschmitt wrote: > type system for nix I’m excited. > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. If GsoC can be made to work, maybe the $5000 (or something like that) can be added? Not sure if that is allowed from the GsoC rules though. -- Proudly written in Mutt with Vim on NixOS. Q: Why is this email five sentences or less? A: http://five.sentenc.es May take up to five days to read your message. If it’s urgent, call me. signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
> Can you give a specific case where your type system would improve things > for either users or developers of nixpkgs? In my experience most of the > nix "code" I write is really just declaration or bash programming, and > it's not clear to me how different types would help. Have you never debugged a "got x but y expected" problem? The typesystem is there, its just lazy as nix is - typed on evaluation. If you write such code it helps: https://github.com/MarcWeber/nixpkgs-haskell-overlay/blob/master/pkgs/haskell-lib.nix But it turned out (oh surpise) that nix is not the best tool to implement a brute force solver for hackage packages in. What about guix https://www.gnu.org/software/guix/ ? Does some typing exist here already? If you need a nice idea about "how to improve the world" - nix guix and the JS implemenation (and the 100+ other distros) clearly say that a cross platform cross language package manage / depndency system is required to derive .nix / guix /whatsoever packages from .. It should allow "platforms" (like Haskell) to have "stable bases" to work on. That would be awesome and the whole open source community & nix would benefit IMHO. Marc Weber ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi Shea, This probably won't have a huge interest for stuff like updating packages (or adding new one), as those are indeed more "scripting", with almost no interaction with the rest of the repo (but still, typed scripting is cool :) ) It becomes however much more useful when dealing with big refactorings (stuff like the switch to multiple-output derivations or changing the organisation of a whole part of nixpkgs). In fact, when looking at the PRs tagged "mass-rebuild" on the nixpkgs repo, more than half of them would benefit from such a system imho. It should also be a huge win for the module system, as things here are much more intricated, and it is easy to silently break a module while changing a different and apparently unrelated one. For some more precise cases, a proper type system would help detecting bugs like [this one](https://github.com/NixOS/nixpkgs/issues/19084), or would have help for things like https://github.com/NixOS/nixpkgs/pull/9607 Hope than answers your question -- Théophane Hufschmitt Thu 12 Jan 17 − 08:25, Shea Levy(s...@shealevy.com) a écrit: > Hi Théophane, > > Can you give a specific case where your type system would improve things > for either users or developers of nixpkgs? In my experience most of the > nix "code" I write is really just declaration or bash programming, and > it's not clear to me how different types would help. > > Thanks, > Shea > > Théophane Hufschmitt writes: > > > Hi, > > > > I am Théophane Hufschmitt, a french master degree CS student, and I > > wish to start a six month length internship on giving nix a type > > system. > > > > Numtide offered to fund a part of the internship, but we still need > > some help for me to be able to start it. > > > > The goal of the internship is to design (and implement) a type system > > for nix in order to be able to statically get some guaranties about > > the well-foundness of the nixpkgs repo (or any nix expression), in > > complement to hydra or travis tests which may let some inconsistencies > > pass − especially on nixos module system which is way harder to test. > > > > Providing nix with a proper type system is a long running issue (see > > https://github.com/NixOS/nix/issues/14), and I think a huge > > opportunity for nix to improve its awesomeness. > > > > The crowdfunding campaign (and a slightly more detailled description of > > the project) is open at https://www.gofundme.com/typing-nix, and you > > are all invited to donate. > > > > Of course, I'll be happy to answer any question, by mail or on > > irc/matrix (I am regnat[m] on freenode). > > > > -- > > Théophane Hufschmitt > > ___ > > nix-dev mailing list > > nix-dev@lists.science.uu.nl > > http://lists.science.uu.nl/mailman/listinfo/nix-dev signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
Re: [Nix-dev] Typing nix − funding campaign
Hi Théophane, Can you give a specific case where your type system would improve things for either users or developers of nixpkgs? In my experience most of the nix "code" I write is really just declaration or bash programming, and it's not clear to me how different types would help. Thanks, Shea Théophane Hufschmitt writes: > Hi, > > I am Théophane Hufschmitt, a french master degree CS student, and I > wish to start a six month length internship on giving nix a type > system. > > Numtide offered to fund a part of the internship, but we still need > some help for me to be able to start it. > > The goal of the internship is to design (and implement) a type system > for nix in order to be able to statically get some guaranties about > the well-foundness of the nixpkgs repo (or any nix expression), in > complement to hydra or travis tests which may let some inconsistencies > pass − especially on nixos module system which is way harder to test. > > Providing nix with a proper type system is a long running issue (see > https://github.com/NixOS/nix/issues/14), and I think a huge > opportunity for nix to improve its awesomeness. > > The crowdfunding campaign (and a slightly more detailled description of > the project) is open at https://www.gofundme.com/typing-nix, and you > are all invited to donate. > > Of course, I'll be happy to answer any question, by mail or on > irc/matrix (I am regnat[m] on freenode). > > -- > Théophane Hufschmitt > ___ > nix-dev mailing list > nix-dev@lists.science.uu.nl > http://lists.science.uu.nl/mailman/listinfo/nix-dev signature.asc Description: PGP signature ___ nix-dev mailing list nix-dev@lists.science.uu.nl http://lists.science.uu.nl/mailman/listinfo/nix-dev
[Nix-dev] Typing nix − funding campaign
Hi, I am Théophane Hufschmitt, a french master degree CS student, and I wish to start a six month length internship on giving nix a type system. Numtide offered to fund a part of the internship, but we still need some help for me to be able to start it. The goal of the internship is to design (and implement) a type system for nix in order to be able to statically get some guaranties about the well-foundness of the nixpkgs repo (or any nix expression), in complement to hydra or travis tests which may let some inconsistencies pass − especially on nixos module system which is way harder to test. Providing nix with a proper type system is a long running issue (see https://github.com/NixOS/nix/issues/14), and I think a huge opportunity for nix to improve its awesomeness. The crowdfunding campaign (and a slightly more detailled description of the project) is open at https://www.gofundme.com/typing-nix, and you are all invited to donate. Of course, I'll be happy to answer any question, by mail or on irc/matrix (I am regnat[m] on freenode). -- 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