You're looking at Less Wrong's discussion board. This includes all posts, including those that haven't been promoted to the front page yet. For more information, see About Less Wrong.

lmm comments on Open thread, September 15-21, 2014 - Less Wrong Discussion

6 Post author: gjm 15 September 2014 12:24PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (339)
Tags: open_thread

Comments (339)

You are viewing a single comment's thread. Show more comments above.

Comment author: lmm 16 September 2014 11:16:41PM *  3 points [-]

I think the problem is hidden beneath the fixed point operator (I've edited the code to be more correct). For Id, is there actually a type Psi such that Psi <~> (Id[Psi] => A)? Isn't that where the Y combinator comes in - the only reason loeb is able to act as a Y combinator is that it gets one passed in via the fixed point lemma? Isn't a fixed point lemma always going to be the same as a Y combinator?

(I wish we were working with a proof that didn't invoke this external lemma)

Comment author: cousin_it 18 September 2014 02:05:28PM *  2 points [-]

I asked the folks on /r/haskell, we hashed out a version in Agda and then I translated it into Haskell. It's not completely in the spirit of the original question, but at least it's a starting point. The code is here, you can try it out on CompileOnline.

ETA: now I also wrote a post about it.

Comment author: cousin_it 17 September 2014 10:40:40AM *  2 points [-]

Hmm, you're right, in a total language you can't define such a Psi for Id. Maybe the type class should go like this:

class Prov p f where
fix :: p (f a -> a (f a))
unfix :: p (a (f a) -> f a)
dup :: p a -> p (p a)
mp :: p (a -> b) -> p a -> p b

I don't know if that's enough. One problem is that fix and unfix are really inconvenient to use without type lambdas, which Haskell doesn't have. Maybe I should try Scala, which has them.

Another problem is in step 13. To do that without soundness, I probably need versions of dup and mp that work inside p, as well as outside. But that makes the type class too complicated.

Powered by Reddit Powered by Reddit