Re: [Nix-dev] Typing nix − funding campaign

[Ludovic Courtès]

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

[Arseniy Alekseyev]

Regarding subtying, I wonder if you're familiar with [1]. This was
described to me as "the right approach to subtyping". I can't myself judge,
but it does sound cool.

1. https://www.cl.cam.ac.uk/~sd601/thesis.pdf

On 30 March 2017 at 08:05, Théophane Hufschmitt  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

[Théophane Hufschmitt]

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

[Théophane Hufschmitt]

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

[Jeaye]

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

[Théophane Hufschmitt]

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

[Danylo Hlynskyi]

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

[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

Re: [Nix-dev] Typing nix − funding campaign

[Rok Garbas]

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

[Maarten Hoogendoorn]

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

[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).
> 


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

[Bardur Arantsson]

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

[Théophane Hufschmitt]

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

[Domen Kožar]

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

[Théophane Hufschmitt]

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

[Vladimír Čunát]

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

[Théophane Hufschmitt]

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

[zimbatm]

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

[Domen Kožar]

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

[Théophane Hufschmitt]

Hi Peter,

Well... That's not exactly how things happened.

First I have to amend myself, my sentence is indeed inexact, it should
have been "The inference algorithm that is *likely* going to be used is no
trivial at all to implement".

The story is that I first discussed with one of my teachers (Didier
Remy, an OCaml core developer and expert on ML type system) about the
opportunity to try typing nix. After some explanations about the
language, it was clear that Hindley-Milner style type inference was
clearly not possible (because of things like the presence of types at
runtime and predicates such as `isInt` or `isString` which fundamentally
break unification). So he asked me to think on how a type system for
nix could look like, and after reflexion, I came up with something that
was roughly the basis of Guiseppe Castagna's − my actual advisor − work
(note that at this time I didn't know at all about his research). That's
why he redirected me to him, and his works are gonna be the main axis
for my work.

But the goal isn't of course to try to apply it regardless of the
alternatives, and that's why the first two months will be devoted for a
large part to the study of the state of the art to determine the best
system to use.

Fri 13 Jan 17 − 10:10, Peter Simons(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

[Peter Simons]

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

[Théophane Hufschmitt]

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

[Théophane Hufschmitt]

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

[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

[Thomas Hunger]

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

[Théophane Hufschmitt]

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

[Théophane Hufschmitt]

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

[Théophane Hufschmitt]

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

[Profpatsch]

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

[Théophane Hufschmitt]

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

[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
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

[Théophane Hufschmitt]

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

[Michael Raskin]

>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

[Maarten Hoogendoorn]

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

[Thomas Hunger]

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

[Peter Simons]

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

[Théophane Hufschmitt]

> 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

[Profpatsch]

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

[Marc Weber]

> 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

[Théophane Hufschmitt]

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

[Shea Levy]

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

[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


signature.asc
Description: PGP signature
___
nix-dev mailing list
nix-dev@lists.science.uu.nl
http://lists.science.uu.nl/mailman/listinfo/nix-dev