Confusing API for creating 'a tys

protz commented 10 years ago

There's a whole variety of functions (declare, fresh, &, /) that have slightly different approaches (they're either constructors or combinators) to declare new types. We should have a single function with some arguments optional that is the single entry point for the module.

Also, our modules should have signatures.

gasche commented 10 years ago

Also, our modules should have signatures.

Daniel, sors de ce corps!

braibant commented 10 years ago

I quite liked the combinators approach, and it was indeed inspired by Daniel's work. I think the useful use case is the following one: you declare one type 'a ty, and then you equip it with an invariant (the "invar" part). I think it should produce a new type descriptor, yet I think it is also important to keep the relationship with the base type descriptor:

if we have to generate elements of the subset type, we can simply look at elements of the base type, and filter the one that meet the invariant
if we have to generate elements of the base type, we can simply look at elements of the subset type.

This is not too important for now, but I think it would be more cumbersome with your new interface.

protz commented 10 years ago

Hmm, good remark. What about just keeping the (/) combinator?

~ jonathan

On Sun 09 Feb 2014 04:43:33 PM CET, Thomas Braibant wrote:

Reopened #16 https://github.com/braibant/articheck/issues/16.

— Reply to this email directly or view it on GitHub https://github.com/braibant/articheck/issues/16.

braibant commented 10 years ago

Closed in b6f199e2d44593472aa660f3c44c536f7cda0ed1

braibant / articheck

Confusing API for creating 'a tys #16