Mercurial > repo
view paste/paste.12027 @ 6946:d634e64cd991
<shachaf> le/rn cut elimination/The cut-elimination theorem states that any Prolog program written using the cut operator ! can be rewritten without using that operator.
author | HackBot |
---|---|
date | Wed, 24 Feb 2016 05:54:46 +0000 |
parents | 8f79561a34c2 |
children |
line wrap: on
line source
2013-01-27.txt:09:43:46: <shachaf> monqy: imo the Await part is like (r,CoYoneda k r) 2013-01-27.txt:09:44:24: <shachaf> monqy: btw are you a CoYoneda expert 2013-01-27.txt:09:45:12: <shachaf> monqy: well you know how CoYoneda IORef = a read-only IORef 2013-01-27.txt:09:47:24: <shachaf> CoYoneda f a = forall r. CoYoneda (r -> a) (f r) 2013-01-27.txt:09:49:50: <shachaf> monqy: anyway when f is a functor CoYoneda f is isomorphic to f?? 2013-01-27.txt:09:50:51: <shachaf> maybe THIS CoYoneda will be more to your liking!!!!!!!!!! http://ncatlab.org/nlab/show/co-Yoneda+lemma 2013-01-28.txt:05:37:44: <shachaf> kmc: By the way, you know ho CoYoneda IORef gives you a "read-only IORef" that can't do any other effects? 2013-02-07.txt:08:55:26: <shachaf> monqy: should i prefer yoneda or coyoneda 2013-02-07.txt:09:06:02: <monqy> shachaf: idk i havent studied them much at all?? my only real "experience" with them is that one time you asked me about how yoneda looks like partially applied >>= and coyoneda like =>>, or something like that 2013-02-07.txt:09:09:06: <shachaf> but coyoneda seems "more obvious to me" 2013-02-07.txt:09:09:33: <shachaf> also coyoneda can be meaningful for things that arne't functors 2013-02-07.txt:09:13:21: <shachaf> ion: do you know what coyoneda is 2013-02-07.txt:09:16:06: <shachaf> "CoYoneda Tree" keeps a tree, and a function to be mapped over it. 2013-02-07.txt:09:17:52: <shachaf> So CoYoneda Tree a = (Tree x, x -> a), for some x. 2013-04-02.txt:23:20:43: <shachaf> CoYoneda is easy. 2013-04-02.txt:23:21:41: <shachaf> CoYoneda is related to Functor. 2013-04-02.txt:23:35:10: <shachaf> Bike: As you probably guessed, Foo is CoYoneda. 2013-04-02.txt:23:37:57: <shachaf> You can treat (CoYoneda IORef) as a read-only IORef, sort of. 2013-04-02.txt:23:38:23: <shachaf> Bike: However: When f is a Functor, CoYoneda f is isomorphic to f 2013-04-02.txt:23:40:54: <shachaf> Bike: btw Yoneda is like CoYoneda except backwards 2013-04-02.txt:23:41:17: <shachaf> I think CoYoneda is more intuitive than Yoneda 2013-04-02.txt:23:57:19: <shachaf> oerjan: What do you think: Yoneda or CoYoneda? 2013-04-02.txt:23:59:13: <shachaf> oerjan: data CoYoneda f a = forall x. CoYoneda (f x) (x -> a) 2013-04-02.txt:23:59:38: <shachaf> when f is a functor it's isomorphic to Yoneda f and to CoYoneda f 2013-04-03.txt:00:00:01: <shachaf> btw Bike did you write lift and lower for CoYoneda 2013-04-03.txt:00:07:28: <shachaf> Where CoYoneda has the *arguments* to fmap, Yoneda has the *result* of fmap. 2013-04-03.txt:00:09:51: <shachaf> I guess you could say: fmap :: CoYoneda f a -> f a 2013-04-03.txt:09:08:43: <shachaf> ais523: Do you prefer one of Yoneda/CoYoneda? 2013-04-03.txt:09:09:23: <shachaf> data CoYoneda f a = forall x. CoYoneda (f x) (x -> a)