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/1be0cbb346d75ee1be8f67d1...