Conversation

patterns are coexpressions

Yes! They're the destructors to the constructors ☺️

Replying to

and

Wouldn't this be the eliminators then? But on second thought I guess that those would still be producing expressions… 🤔

Replying to

and

Could be, I sometimes confuse the two 😅

Replying to

and

Constructor: Cons 1 Nil Pattern: length (Cons _ xs) = 1 + length xs Eliminator: tail xs Copattern: head (repeat x) = x tail (repeat x) = repeat x

Replying to

and

Patterns are eliminators. The µµ̃ calculus and especially System L (see Downen's thesis) surface this really beautifully IMO!