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`,…
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…
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.
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`,…
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…
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.