A couple of months ago I was playing around with a similar technique, Mogensen-Scott encoding, in typescript. I was mainly interested in it as a way to express

A couple of months ago I was playing around with a similar technique, Mogensen-Scott encoding, in typescript. I was mainly interested in it as a way to express sum types without a bunch of if statements (instead a "value" of a type takes functions for each possible case branch and calls the appropriate one). I ended up writing a little dependent type checker: https://gist.github.com/dunhamsteve/1be0cbb346d75ee1be8f67d192e73234 https://gist.github.com/dunhamsteve/1be0cbb346d75ee1be8f67d1...