jozefg

It's not an isomorphism though, it misses the always true map. This means that many predicates on nat do not terminate on nat -> bool.

So this article shows how to check equality on `(nat -> bool) -> bool`. Your question, I think, is to figure out how to check `nat -> bool` for equality.

The issue is that there are more operations we can do with `nat`, more properties we can check, than there are with `nat -> bool`. With `nat -> bool` we can basically check `i` indices and so the behavior of any predicate `(nat -> bool) -> bool` is basically determined by the first `i` indices. And that's finite. This algorithm is basically implicitly finding the indices considered by the supplied predicate and then brute-forcing all those entries.

With `nat` there's no such finite cut off point. It's never the case that it suffices to test a predicate `nat -> bool` on finitely many entries to fully determine it. So we cannot do the same brute force search.

It is possible in certain cases, that's the point of the article. One of the contributors to HoTT is the author of the paper introducing these algorithms :)

This algorithm is only total if the predicates supplied are total. Since `x == one AND x == zero` is not total the algorithm will diverge. It will not return the incorrect answer though.

I'm glad you're enjoying it :)

Be careful with writing that compiler, I decided to add a type system to my hobby language a while back and now I'm doing research in type theory. It's a slippery slope.

I actually host the main repo on my (https://bitbucket.org/jozefg/pcf). I've just found that most people would prefer to see the GitHub version (for starring, more pleasant forking, better code viewing) so I usually link there.

I generally duplicate my repos on bitbucket/github so I can feel smug when one goes down for a while.

It's not a bad skill to be able to read SML/OCaml. They're really very similar to Haskell and actually pretty fun to write.

I suppose you could have inferred (ha) I feel that way from this blog post though :)

It does, it's ambiguous to have `Constructor.fun` for this reason.