Unifying case statements and records

[tysonzero]

As discussed here case statements on variants are effectively equivalent to records of functions. So I thought I would make GitHub issue to discuss people's thoughts on such an approach.

[willtim]

I really like this idea. The key benefit I think, is that the set of choices given for case analysis are just a record of functions (or an arbitrary expression that evaluates to a record of functions). It does still need some design though, it's not yet clear to me how "open variants" are handled. In the existing design, we use a syntax analogous to record extension, e.g. λ> let f = x -> case x of { Foo x -> x, Bar{x,y} -> x+y | r -> 42 } λ> f (Baz{}) 42

[tysonzero]

So it seems like the core function for this is the following:

case : forall as bs c. {map (-> c) as} -> (<bs> -> c) -> <as + bs> -> c

Which would handle open records via the second argument, and to handle closed variants you can just pass in absurd as the second argument.

So your example would be:

let f = case { Foo x = x, Bar {x, y} = x + y } (_ -> 42)
f (Baz {})
42

[tysonzero]

After further thought i'm not 100% sure what the best primitives are, I have also been thinking about something like:

(=>) : forall as b. <as> -> {map (-> b) as} -> b

split : forall as bs c. (<as> -> c) -> (<bs> -> c) -> <as + bs> -> c

If anonymous sums were supported as in the other issue, you could replace the above with something like:

split : forall xss. <fold xss> -> Sum (map Variant xss)

Part of why I am thinking about => and split or similar is it makes implementing something like the following easier:

mcase : forall as bs. {map (-> c) as} -> <as + bs> -> Maybe c
mcase fs v = split (=> fs) (_ -> Nothing {}) v