Support Proper's Deriving of Types

[zkessin]

What would be required to be able to derive types as the Erlang implementation does?

[alfert]

See #3, #4 and #5. There are/were some rudiments in my codebase. It requires to re-implement a big part of proper.

[zkessin]

I am happy to help FWIW

[turion]

I don't really understand the issues 3 - 5 you cited. Is there a fundamental problem, or is it just a lot of work?

[alfert]

Back in time - if I remember right and 3 years is a lot of time - I recognised that parsing/handling of more interesting types in Proper was done on a source code level, ie. there are differences between Erlang and Elixir. To handle this properly means that you need understand the Elixir encoding of types, unparse them to Erlang syntax and after that deal with the undocumented internal type server from Proper. So it is an arbitrary big set of work with a questionable result if you consider the arguments of Jesper Andersen (see the readme). A better approach would be that the internals of PropEr are fixed (i.e. no Erlang syntax for types), but I do not know whether this has ever happened. There are some refactorings in Proper for supporting Targeted PBT, but I did not check the details. Proper is quite complex inside and not for the faint of heart.

I won't do it, but I am happy about PRs. But currently I am way more interested in understanding Targeted PBT, its usage patterns and how to provide a stable interface for that in Elixir (my current solution and its tests are flaky).

[zkessin]

I just did a talk on using types in Erlang/ elixir, I am uploading it to youtube as I type this

https://youtu.be/48phgMNV0AA

[evnu]

I implemented a small library propcheck_derive to derive generators from @type. It is still a little bit rough, but I wanted to finally publish it so that others might be able to make some use of it. propcheck_derive disallows cyclic types and creates very simple generators. I'd be willing to spent some more time on the implementation (there are a lot of FIXMEs left) if there is interest in it.