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

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