Interesting TyDe talk by on defining inductive type families (called "indexed types" in the talk) by specifying patterns that select a constructor instead of specifying the types of their constructors.
Conversation
One thing I was wondering while watching is if it was possible to somehow 'upgrade' pattern matching to let you write these things as pattern matches? Ie. with tagged cases and overlaps. Seems like it would be more a logic language then though… like Twelf maybe?
1
1
It would lead to other issues though which runs counter to the goals of simplification… like you might want a way to constrain pattern matching again so that you can do regular programming. So might not actually be that useful 😅
Might lead to something like Mercury's modes and determinism checking which is very much _not_ simple. 😬
1