5 ms·
Here's proof that the last two parts are isomorphic: to :: (a -> [b]) -> (a -> (forall r . (b -> r -> r) -> r -> r)) to f a = h (f a) where
by DanWaterworth 12y ago
Here's proof that the last two parts are isomorphic:
to :: (a -> [b]) -> (a -> (forall r . (b -> r -> r) -> r -> r))
to f a =
h (f a)
where
h :: [b] -> (forall r . (b -> r -> r) -> r -> r)
h b cons nil =
case b of
(x:xs) -> cons x (h xs cons nil)
[] -> nil
from :: (a -> (forall r . (b -> r -> r) -> r -> r)) -> (a -> [b])
from f a = f a (:) []
- NotAtWork 12y agoThank you. That step had me really confused.
- tel 12y agoThe fast way is to say that [b] is the initial algebra of the functor (Maybe . (b,)) and then note that initial algebras are representable as newtype Mu f = Mu (forall r . (f r -> r) -> r)
- DanWaterworth 12y agoInteresting. I'm not well versed in these things yet, but I've seen: forall r . (f r -> r) -> r before. Am I right in saying it's the type of a catamorphism? In which case, yes, it makes total sense that your `Mu` type is equivalent to the (possibly) more usual: newtype Mu f = Mu (f (Mu f))
- tel 12y agoYep! You can think of it as a "frozen catamorphism" or the "right half" of foldr when you specialize `f`. The really fascinating part is that my Mu is equivalent to your Mu in Haskell... because it's Turing complete. In a world where least and greatest fixed points differ, in a world where data and codata differ, then Mu has a cousin Nu data Mu f = Mu (forall r . (f r -> r) -> r) data Nu f = forall r . Nu (r -> f r) r where Mu generates the data and Nu generates the codata. You'll recognize Nu as a frozen anamorpism, of course. If you want a total language, replace generalized fixed points with these two pairs of fixed points. Mu only lets you construct things finitely and tear them down with catamorphisms and Nu only lets you destruct things finitely which you've built with anamorphisms. Even in Haskell you can treat certain uses of types as being data-like or codata-like by viewing them more preferentially through Mu or Nu---though you can always convert both to Fix newtype Fix f = Fix (f (Fix f))
- rebcabin 12y agoI'd be grateful for a pointer to some fundamental background reading; I can only follow enough of your reasoning to be intrigued and committed to learning more :)
- tel 12y agoI'm trying to write up a blog post about this now. A really good presentation focused on types and programming languages is available in the middle chapters of Practical Foundations for Programming Languages. I originally learned about it from studying Aczel's Antifoundation Axiom from Barwise and Moss' Vicious Circles[0]---in there you can get a much more mathematical foundationalist POV---but Harper's book is more direct. [0]http://www.amazon.com/Vicious-Circles-Center-Language-Information/dp/1575860082 http://www.amazon.com/Vicious-Circles-Center-Language-Inform...
- moomin 12y agoIs this quite right? Sorry this is a bit vague/unclear, but what happens if you, say, call the reduction function, throw the result away and then call it again? I ran this example through Clojure in let's write a transducer, and it plain doesn't work; I think the mapping given above works for all transducers that are actually valid, but I think the type definition allows for broken ones. Again, I'm not sure & still learning, so please explain if I've gone wrong here.
- tel 12y agoIf you throw the result away in pure code then you may as well have never computed it: the second result holds only. In an impure setting none of the math above holds. Edit: note that this doesn't mean you have to throw away local or global state. You can recapture that by using state machine transformers or even Kleisli state machine transformers (although that gets pretty heavy!)
- moomin 12y agoAaah. Makes sense. I couldn't figure out why the reasoning seemed sound, but I had something that didn't match. It's because in Clojure, r has state itself.