willtim / Expresso

A simple expressions language with polymorphic extensible row types.
Other
300 stars 15 forks source link

Why are literal variants open by default? #8

Closed FrankBro closed 5 years ago

FrankBro commented 6 years ago

Sorry, this isn't really an issue, more a question. I've been interested into row polymorphism and found your implementation of it very helpful. I've seen this in many implementations but never found why.

Why are literal variants open by default? Is there any technical reason or just some logical reason I fail to see?

Once again, great work on this implementation.

sboosali commented 6 years ago

idk, but extensible variants are useful for Exceptions (which is why it's pretty much an empty type class in Haskell).

On Mon, Aug 20, 2018, 7:32 PM Francois Brodeur notifications@github.com wrote:

Sorry, this isn't really an issue, more a question. I've been interested into row polymorphism and found your implementation of it very helpful. I've seen this in many implementations but never found why.

Why are literal variants open by default? Is there any technical reason or just some logical reason I fail to see?

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/willtim/Expresso/issues/8, or mute the thread https://github.com/notifications/unsubscribe-auth/ACNoMTPN2B6r9K8c5KdFj9Qj1EWkkN7qks5uS0cfgaJpZM4WE3an .

willtim commented 6 years ago

AFAIK, open variants just happen to be the most useful default, it's also the opposite (dual) of closed which is what works best as a default for records. If closed variants were the default, then your example:

let div = n d -> if d == 0 then DivBy0 {} else Ok (n / d)

would not typecheck since the "if" form has the type "forall a. Bool -> a -> a -> a"; and "a" cannot unify to a variant that has both DivBy0 and Ok unless the variant terms at both branches are open.

FrankBro commented 6 years ago

I've been playing with writing my own compiler and I was wondering if I was gonna support open/close via a keyword. In the div example, every cases are covered and therefore, being able to easily define a closed set of possibility might be useful? Just an idea I had, will try to report once I support this.

willtim commented 6 years ago

Yes being able to define a closed-set is very useful and this can be done in Expresso using type signatures. For your example, you could write:

λ> let div = (n d -> if d == 0 then DivBy0 {} else Ok (n / d)) : Int -> Int -> <DivBy0 : {}, Ok : Int>

But perhaps a better idea would be to create smart constructors for closed-variants types as described in https://github.com/willtim/Expresso#closed-variants

What would be a good idea is some sort of syntactic sugar for defining such smart constructors, is that what you have in mind? I think you would have to define the set collectively, like Haskell's "data" declaration.

willtim commented 5 years ago

I will assume this is now answered.