jozefg

4 ms·

1.
by jozefg 8y ago
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.
2.
by jozefg 8y ago
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 proper
3.
by jozefg 8y ago
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 :)
4.
by jozefg 8y ago
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.
5.
by jozefg 11y ago
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.
6.
by jozefg 12y ago
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 usual
7.
by jozefg 12y ago
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 :)
8.
by jozefg 12y ago
It does, it's ambiguous to have `Constructor.fun` for this reason.