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

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

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.

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

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

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,

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

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

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

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 :) > > > -- > >

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

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

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

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

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 :)

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

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

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

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

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

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

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

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

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

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,

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

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

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

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

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

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

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,

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

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

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

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

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

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

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

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

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

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

[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