Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What is the name of this functor that uses RankNTypes?

During play around objective package, I noticed following type has interesting property.

> {-# LANGUAGE RankNTypes #-}
> data N f r = N { unN :: forall x. f x -> (x, r) }

It is a Functor.

> instance Functor (N f) where
>    fmap f (N nat) = N $ fmap (fmap f) nat
>          -- or,   = N $ \fx -> let { (x,a) = nat fx } in (x, f a)

After few hours of google/hoogle, I gave up finding any existing module that includes this type. What is this type? If it is well known, what is the name? Is this useful or ignored because useless?

This is not my 100% original creation, because N was derived from Object found in objective package.

> data Object f g = Object {
>     runObject :: forall x. f x -> g (x, Object f g)
>   }

N f is a Functor which yields Object f Identity when Fix is applied to.


Following is a fact about this type and why I thought it is interesting.

N converts Reader to Writer, vice versa. (Here I used (=) symbol for isomorphism between types)

N ((->) e) r
 = forall x. (e -> x) -> (x, r)
 = (e, r)

N ((,) d) r
 = forall x. (d, x) -> (x, r)
 = d -> r

N converts Store comonad to State monad, but inverse is not true.

> data Store s a = Store s (s -> a)
> type State s a = s -> (s, a)

N (Store s) r
 = forall x. (s, (s -> x)) -> (x, r)
 = forall x. s -> (s -> x) -> (x, r)
 = s -> (s, r)
 = State s r

N (State s) r
 = forall x. (s -> (s, x)) -> (x, r)
 = forall x. (s -> s, s -> x) -> (x, r)
 = forall x. (s -> s) -> (s -> x) -> (x, r)
 = (s -> s) -> (s, r)  -- ???

N can't take Maybe.

N Maybe r
 = forall x. Maybe x -> (x, r)
 = forall x. (() -> (x, r), x -> (x, r))
 = Void     -- because (() -> (x, r)) can't be implemented

Following function may be fun. I couldn't do it's inverse.

> data Cofree f a = Cofree a (f (Cofree f a))
> data Free f a = Pure a | Wrap (f (Free f a))

> unfree :: Free (N f) r -> N (Cofree f) r
> unfree (Pure r) = N $ \(Cofree a _) -> (a, r)
> unfree (Wrap n_f) = N $
>   \(Cofree _ f) -> let (cofree', free') = unN n_f f
>                    in unN (unfree free') cofree'

Entire post is literate Haskell (.lhs).

like image 742
viercc Avatar asked Apr 29 '16 03:04

viercc


2 Answers

I call it a "handler" functor. Object used to be defined using the handler functor before I released objective.

Yeah, this functor is interesting -- Cofree (Handler f) has a public getter and Free (Handler f) is a mortal object. Maybe I should have shipped the handler functor...

like image 92
fumieval Avatar answered Oct 30 '22 00:10

fumieval


Although it is already answered, I found another answer to the question by myself.

Type N was the value-level representation of the type class Pairing, described in following articles.

Free for DSLs, cofree for interpreters

Cofree Comonads and the Expression Problem (Paring is called Dual here)

Pairing and N are same things

The definition of Pairing is this.

> class Pairing f g where
>   pair :: (a -> b -> c) -> f a -> g b -> c

f and N f is Pairing.

> instance Pairing f (N f) where
>   pair k fa nb = uncurry k $ unN nb fa

N can be represented in terms of Pairing.

> data Counterpart f r = forall g. Pairing f g => Counterpart (g r)
>
> iso1 :: N f r -> Counterpart f r
> iso1 = Counterpart
>
> iso2 :: Counterpart f r -> N f r
> iso2 (Counterpart gr) = N $ \fx -> pair (,) fx gr

There is a Free-vs-Cofree instance, that corresponds to my unfree. Other interesting instances are also defined in the articles.

> instance Pairing f g => Pairing (Free f) (Cofree g) where
>   pair = undefined -- see link above

Extending Pairing to PairingM to Object

Former article goes to extending Pairing to do computation inside a Monad m.

> class PairingM f g m | f -> g, g -> f where
>   pairM :: (a -> b -> m r) -> f a -> g b -> m r

If we rewrite PairingM to a form similar to N, we get the Object again.

> -- Monad m => HandlerM' f m r ~ HandlerM f m r
> data HandlerM' f m r = forall g. PairingM f g m => HandlerM' (g r)
> data HandlerM f m r = HandleM { runHandlerM :: forall x. f x -> m (x, r) }
>
> -- Fix (HandlerM f m) ~ Object f m
> -- Free (HandlerM f m) ~ (mortal Object from f to m)
like image 1
viercc Avatar answered Oct 30 '22 02:10

viercc