search

thufschmitt / ptyx

A type-system for Nix
BSD 3-Clause "New" or "Revised" License
96 stars 3 forks source link

Current state of ptyx #8

Open GuillaumeDesforges opened 4 years ago

GuillaumeDesforges commented 4 years ago

Hi, is the project alive? Do you plan on continuing to work on it?

Thanks

thufschmitt commented 4 years ago

Hi,

No, I'm not working on this anymore − I think getting this to work correctly is too much work compared to what we can gain from it

sgraf812 commented 4 years ago

Could you maybe state what exactly were the problems that you think were too much work? I brainstormed what a type inference engine could look like with a colleague. We figured that the dynamic semantics of with and // are quite hard to express statically and then went on to google for existing attempts like this project first.

So, did you have similar problems with the most general (inferrable) type of with and //? Did you use row polymorphism or plain old subtyping for records? Are there any other problems that we aren't even aware of yet?

thufschmitt commented 4 years ago

Sorry for the very late answer. The reason why this is too much work is that this tried to be compatible with most of the existing code, including constructs such as x: if isInt x then x+1 else if isList x then ["foo"] ++ x else x which require a heavy use of union/intersection types and require you to annotate nearly everything (which is a pain in practice).

The typing of records is also based on intersection types, essentially borrowed from https://www.irif.fr/~gc/papers/covcon-again.pdf#subsection.4.5.

with is something I mostly let aside because it's a bit painful, but with union types and a good-enough typing of records there's no big theoretical issue with it. The only issue is that it risks to make all the types very messy (because if foo is a mostly-unknown record, then with foo means that there can be all sort of crap in the environment and the types have to reflect that).