Has anyone looked into Church encoding in the type system?

1

I wondered if it could be done. The runtime value and the type system representation match up.

I knew you could use church encoding to encode integers, but here the GADTs allow the type representation to have the same depth and therefore the same value and ability to discern,

typesystem counting trace
typesystem counting trace885×224 37.6 KB

typesystem counting
typesystem counting666×480 49.1 KB

2

Intriguing, but you’re suffering from the curse of knowledge here. Some context on what it is, why it’s interesting at all and why you’re doing that would be nice. The same applies to your other post about `Eff`.

1 Like
3

If there’s no takers, there’s no takers.
There’s nothing stopping you asking a question, and there’s plenty written about the terms I’m using.