The Comonad.Reader » Type Theory http://comonad.com/reader types, (co)monads, substructural logic Thu, 02 May 2013 14:19:12 +0000 http://wordpress.org/?v=2.8.4 en hourly 1 Homotopy and Directed Type Theory Slides http://comonad.com/reader/2011/homotopy-and-directed-type-theory-slides/ http://comonad.com/reader/2011/homotopy-and-directed-type-theory-slides/#comments Fri, 28 Oct 2011 02:38:34 +0000 Edward Kmett http://comonad.com/reader/?p=425 As requested, here are the slides from Dan Doel's excellent presentation on Homotopy and Directed Type Theory from this past Monday's Boston Haskell.

]]>
http://comonad.com/reader/2011/homotopy-and-directed-type-theory-slides/feed/ 0
Generatingfunctorology http://comonad.com/reader/2008/generatingfunctorology/ http://comonad.com/reader/2008/generatingfunctorology/#comments Wed, 14 May 2008 07:45:38 +0000 Edward Kmett http://comonad.com/reader/2008/generatingfunctorology/ Ok, I decided to take a step back from my flawed approach in the last post and play with the idea of power series of functors from a different perspective.

I dusted off my copy of Herbert Wilf's generatingfunctionology and switched goals to try to see some well known recursive functors or species as formal power series. It appears that we can pick a few things out about the generating functions of polynomial functors.

As an example:

 
Maybe x = 1 + x
 

Ok. We're done. Thank you very much. I'll be here all week. Try the veal...

For a more serious example, the formal power series for the list [x] is just a geometric series:

 
[x] = mu y . 1 + x y  -- the mu here is a pleasant fiction, more below
    = 1 + x (1 + x (1 + x (...)))
    = 1 + x + x^2 + x^3 + ...
    = 1/(1-x)
 

Given the power series of a functor, its nth coefficient * n! tells you how many distinguishable ways its constructors can house n values. If we see that a list of n values can be permuted n! ways this has some interesting possibilities for linearizing the storage of some functors. The list case is boring, we can store a finite list of n elements by supplying the length of the array and an array of n elements, hence (among other reasons) the mu above.

Lets try decorated binary trees:

 
data Tree x = Leaf | Node (Tree x) x (Tree x)
 
Tree x = mu y. 1 + x * y * y
       = 1 + x * (1 + x * (...)^2)^2
       = 1 + x + 2x^2 + 5x^3 + 14x^4 + 42x^5 + ...
 

It turns out the coefficients of our generating function are the Catalan numbers, A000108, commonly denoted C(n), which happen to be well known for among other things, being the number of ways you can build a binary tree of n nodes.

This tells us we could store a tree by storing a number n of nodes it contains, an array of that many nodes, and an index 0 < = i < C(n) to tell you which particular tree you selected. Not that this is likely to be an incredibly time-efficient encoding, but you could then fmap over the tree by just fmapping over your array.

For a formal power series,

$f(x) = \sum_{i=0}^{\infty} a_n x^n = a_0 + a_1 x + a_2 x^2 + ... $

its derivative is given by differentiating the series term by term:

$f'(x) = \sum_{i=1}^{\infty} n a_n x^{n - 1} = a_1 + 2 a_2 x + 3 a_3 x^2 + ...$

Consequently we can take the derivative of a list:

([]') x = 1 + 2x + 3x^2 + ... = 1/(1-x)^2 = ([] :*: []) x

and rederive the notion that a derivative/one hole context of a list can be represented by a pair of lists.

If we step slightly outside of the Haskell users' comfort zone and notion of a Functor and allow other Species, we get (as noted by apfelmus the other day) that Exp a is just a bag of elements with no predetermined order.

 
Exp x = 1 + x + x^2/2! + x^3/3! + ... = Bag x
 
Since there are n! ways to order n elements and Bag manages to forget that information, we can get a feeling for the meaning of division in this setting.
 
Similarly we can define:
<pre lang="haskell">
Sinh x = x + x^3/3! + ... -- a Bag of some odd number of elements.
Cosh x = 1 + x^2/2! + ... --  a Bag of some even number of elements.
 

Then by construction:

 
Exp = Cosh :+: Sinh
 

The derivative of Exp is Exp, of Cosh is Sinh, of Sinh is Cosh, all as you would expect.

We can handle other species as well:

 
Cycle a = 1 + x^2/2 + x^3/3 + x^4/4 + ... -- cycles
Cycle_n a = x^n/n -- cycles of n elements
Bag_n a = x^n/n!  -- bags of n elements
 

That said, there seem to be some problems, not every functor is well behaved in this way. Lets take for instance the type of natural numbers given by the functor:

 
data Nat a = S (Nat a) | Z
 

Then the recurrence blows up, the coefficient for 0 is $\aleph_0$!

Similarly, if we parameterized a functor on another value we have to deal with the number of cases that other value can denote.

 
Either a x = |a| + x
(a,x) = |a| x
 

This is both good and bad, using the above, we can quickly establish an isomorphism between Either () and the Maybe Functor, but we blow up again for Either Integer. This gets even worse if we allow 'functors in space.' (i.e. functors that can contain functions)

On the other extreme, we might modify our tree example and remove the leaves, yielding infinite decorated cotrees.

 
Tree x = nu y. x * y * y
       = x * (x * (...)^2)^2
       = 0 + 0x + 0x^2 + 0x^3 + ...
 

Then a_n = 0 for all n in the natural numbers, so you can't use the coefficients of the generating function to tell you about the behavior of an infinite structure! It would appear that the generating function of a functor does not capture what happens in the greatest fixed point case, so we can only use generating functions to describe the behavior of data defined with mu, not in general codata defined by nu.

The Bags and Cycles above are nice examples, but if we wanted to rule out the non-polynomial Functors (from the Haskell perspective) in the above then we can simply limit ourselves to ordinary generating functions with natural number coefficients, that is to say generating functions of the form:

$f(x) = \sum_{i=0}^{\infty} a_n x^n = a_0 + a_1 x + a_2 x^2 + ... $

To choose to admit bags, cycles and other species etc. then you need merely also permit exponential generating functions with natural coefficients, that is to say, generating functions of the form:

$f(x) = \sum_{i=0}^{\infty} a_n x^n / n! = a_0 + a_1 x / 1! + a_2 x^2 / 2! + ... $

]]>
http://comonad.com/reader/2008/generatingfunctorology/feed/ 12
Towards Formal Power Series for Functors http://comonad.com/reader/2008/towards-formal-power-series-for-functors/ http://comonad.com/reader/2008/towards-formal-power-series-for-functors/#comments Tue, 13 May 2008 09:22:19 +0000 Edward Kmett http://comonad.com/reader/2008/towards-formal-power-series-for-functors/ = 6.9, since it uses type families. There has been a lot of posting recently about automatic differentiation in Haskell, and I wanted to try the same thing with functors in the spirit of Conor McBride's Clowns to the Left of me, Jokers to the [...]]]> The post below will only compile on a version of GHC >= 6.9, since it uses type families.

There has been a lot of posting recently about automatic differentiation in Haskell, and I wanted to try the same thing with functors in the spirit of Conor McBride's Clowns to the Left of me, Jokers to the Right and The derivative of a regular type is its type of one hole contexts, figuring that a Power Series could fully generalize Christophe Poucet's Higher Order Zippers, and might provide me with a neat extension to the zipper comonadic automata I've been aluding to recently.

 
{-# OPTIONS -fglasgow-exts -fallow-undecidable-instances -fallow-overlapping-instances #-}
module Derivatives where
import Control.Monad.Identity
import Control.Arrow ((+++),(***),(&&&))
import Data.Monoid
infixl 9 :.:
infixl 7 :*:
infixl 6 :+:
 

To avoid importing category-extras and keep this post self-contained (modulo GHC 6.9!), we'll define some preliminaries such as Bifunctors:

 
class Bifunctor f where
	bimap :: (a -> c) -> (b -> d) -> f a b -> f c d
 
instance Bifunctor (,) where
	bimap f g ~(a,b) = (f a, g b)
 
instance Bifunctor Either where
	bimap f _ (Left a) = Left (f a)
	bimap _ g (Right b) = Right (g b)
 

Constant functors:

 
data Void
instance Show Void where show _ = "Void"
newtype Const k a = Const { runConst :: k } deriving (Show)
type Zero = Const Void
type One = Const ()
instance Functor (Const k) where
	fmap f = Const . runConst
 

and functor products and coproducts:

 
newtype Lift p f g a = Lift { runLift ::  p (f a) (g a) }
type (:+:) = Lift Either
type (:*:) = Lift (,)
instance Show (p (f a) (g a)) => Show (Lift p f g a) where
	show (Lift x) = "(Lift (" ++ show x ++ "))"
instance (Bifunctor p, Functor f, Functor g) => Functor (Lift p f g) where
	fmap f = Lift . bimap (fmap f) (fmap f) . runLift
 

and finally functor composition

 
newtype (f :.: g) a = Comp { runComp :: f (g a) } deriving (Show)
instance (Functor f, Functor g) => Functor (f :.: g) where
	fmap f = Comp . fmap (fmap f) . runComp
 

So then, an ideal type for repeated differentiation would look something like the following, for some definition of D.

[Edit: sigfpe pointed out, quite rightly, that this is just repeated differentiation, and apfelmus pointed out that it not a power series, because I have no division!]

 
newtype AD f a  = AD { runAD :: (f a,  AD (D f) a) }
 

As a first crack at D, you might be tempted to just go with a type family:

 
{-
type family D (f :: * -> *) :: * -> *
type instance D Identity = One
type instance D (Const k) = Zero
type instance D (f :+: g) = D f :+: D g
type instance D (f :*: g) = f :*: D g :+: D f :*: g
type instance D (f :.: g) = (D f :.: g) :*: D g
-}
 

This could take you pretty far, but unfortunately doesn't adequately provide you with any constraints on the type so that we can treat AD f as a functor.

So, we'll go with:

 
class (Functor (D f), Functor f) => Derivable (f :: * -> *) where
	type D f :: * -> *
 

and cherry pick the instances necessary to handle the above cases:

 
instance Derivable Identity where
	type D Identity = One
 
instance Derivable (Const k) where
	type D (Const k) = Zero
 
instance (Derivable f, Derivable g) => Derivable (f :+: g) where
	type D (f :+: g) = D f :+: D g 
 
instance (Derivable f, Derivable g) => Derivable (f :*: g) where
	type D (f :*: g) = f :*: D g :+: D f :*: g
 
instance (Derivable f, Derivable g) => Derivable (f :.: g) where
	type D (f :.: g) = (D f :.: g) :*: D g
 

With those instances in hand, we can define the definition of a Functor for the automatic differentiation of a Functor built out of these primitives:

 
instance (Derivable f, Functor (AD (D f))) => Functor (AD f) where
	fmap f = Power . bimap (fmap f) (fmap f) . runPower
 

Unfortunately, here is where I run out of steam, because any attempt to actually use the construct in question blows the context stack because the recursion for Functor (AD f) isn't well founded and my attempts to force it to be so through overlapping-instances have thus-far failed.

Thoughts?

[Source Code]

]]>
http://comonad.com/reader/2008/towards-formal-power-series-for-functors/feed/ 12
Parameterized Monads in Haskell http://comonad.com/reader/2007/parameterized-monads-in-haskell/ http://comonad.com/reader/2007/parameterized-monads-in-haskell/#comments Fri, 13 Jul 2007 07:46:15 +0000 Edward Kmett http://comonad.com/reader/2007/parameterized-monads-in-haskell/ Recently Eric Kidd and Dan Piponi have used a bit of type hackery by Oleg Kiselyov and -fno-implicit-prelude to build some interesting restricted monads, like the Wadler Set and Bag monads.

There is another interesting monad variation - a parameterized monad - where the monad carries around an additional parameter at the type level such as a type-level set of effects. One really good example of this is the separation logic monad in Hoare Type Theory. The pre- and post- conditions can be viewed as the parameter carried around on that monad. Wadler and Thiemann, Jean-Christophe Filliâtre and others have explore this notion for encoding effects.

This prompts the question of if parameterized monads can be implemented directly in Haskell. Indeed they can, but a simple version fails with the signature:


class BadHaskell m p p' p'' | p p' -> p'' where
return :: a -> m p a
fail :: a -> m p a
(>>=) :: m p a -> (a -> m p' a) -> m p'' a

This of course runs afoul of the fact that all of the parameters are not mentioned in return, so we have to break it apart into two or three classes.


class Return m p where
return :: a -> m p a

class Fail m p where
fail :: String -> m p a

class Bind m p p' p'' | p p' -> p'' where
(>>=) :: m p a -> (a -> m p' a) -> m p'' a

By splitting off fail, we can make it so that it is illegal to use an incomplete pattern on certain monads, a small win, but it may be useful in a later post.

However, there turns out to be quite some awkwardness from the perspective of type inference with this type. In particular we are used to the types of our monads being able to be inferred from the type of their results, but we lose this inference on return. Moreover, we can't just use existing monads under this syntax, we'd have to lift them into a newtype that accepted the additional parameter.

Ignoring the problems with existing monads, and correcting the type inference problem directly by adding fundeps doesn't help as


class Bind m p p' p''
| p -> p' p''
, p' -> p p''
, p'' -> p p'
where
(>>=) :: m p a -> (a -> m p' a) -> m p'' a

is too restrictive and could be shown that under a strict interpretation of the laws, would never be able to be made to satisfy the monad laws except in the base case, because of the inability to construct an associative operation combining the parameters that isn't trivial.

As an aside, speaking of failing monad laws, it is interesting to note that the Set restricted monad actually fails a monad law given that functions in haskell need not respect equality, since x = y => f x = f y fails to hold in general for user defined equality as used by the Set monad, as noted by Andrea Vezzosi on #haskell, the order of association can make a difference as to the result of the computation. This is arguably a minor quibble as you wouldn't be using it unless you knew the type you were going to pass around and how your functions worked on it with respect to its notion of equality.

Turning back to the issue of being unable to pass traditional monads into this type, we realize that having a separate m and p parameters to the type class is redundant as you can generate an equivalent notion by letting m vary.


class Return m where
return :: a -> m a

class Fail m where
fail :: String -> m a

class Bind m m' m'' | m m' -> m'' where
(>>=) :: m a -> (a -> m' a) -> m'' a

This still has the problem that the type of return is not inferable, but now at least we can derive instances of these classes for instances of Monad. Of course, if we create a generic instance for


import qualified Control.Monad as Old
instance Old.Monad m => Bind m m m where (>>=) = (Old.>>=)
...

we then run afoul of the fact that we can't define any other interesting instances because the compiler won't know which way to go with type class inference.

However, even without that we can import each monad in turn, and define some interesting interfaces between them:


instance Bind Maybe [] [] where
Just a >>= f = f a
Nothing >>= _ = []

-- testMaybeList :: [Int] = [2,4]
testMaybeList = Just 2 >>= \x -> [x*1,x*2]

Admittedly there is an n^2 combinatorial explosion of combinations and not all of them have clear semantics, but we can choose to implement only the ones that have an unambiguous interpretation and leave off the rest and pay as we go, implementing them as needed. A more mature version of this might provide an interesting alternative/supplement to the MTL approach and can be viewed as a limited fragment of Lüth and Ghani's monad composition through coproducts.

However, we still haven't solved the return problem, but it turns out that monad laws can come to the rescue.

If we start to implement a number of these we notice a pattern when it comes to the Identity monad. In general we can define instances of Bind for the Identity monad for any monad presuming we can liftM, to handle the case on the right, but since liftM requires a sort of circular dependency loop, we choose to make Bind enforce the availability of fmap, allow overlapping instances, and then define:


class (Functor m, Functor m', Functor m'') => Bind m m' m''
| m m' -> m''
where
(>>=) :: m a -> (a -> m' b) -> (m'' b)
(>>) :: m a -> m' b -> m'' b
m >> k = m >>= const k

instance Functor a => Bind Identity a a where
m >>= f = f (runIdentity m)

instance Functor a => Bind a Identity a where
m >>= f = fmap (runIdentity . f) m

-- and to disambiguate between the above instances...
instance Bind Identity Identity Identity where
m >>= f = f (runIdentity m)

The correctness of this is in fact enforced by the monad laws as these instances can be read as the familiar laws once you remove the noise of the Identity monad:


return m >>= f = f m
m >>= return . f = fmap f m
return m >>= f = f m

This gives us a single natural notion of return for all monads that we can use and still glue together via >>=:


class Return m where
returnM :: a -> m a

return :: a -> Identity a
return = Old.return

Now the problem is if you write a statement like return 2 >>= \x -> return (x+1), you can have the Identity type percolate out of your monad expression, even when you were expecting a ListT or State monad or something more interesting, so we need a way to transform values from the Identity monad to an arbitrary monad for use when you want its type to conform to an external signature.


class Go n m where
go :: n a -> m a

instance Return a => Go Identity a where
go = returnM . runIdentity
instance Go a a where
go = id

So, now we can tell our code to go (do something) and it will transform any lingering Identities to whatever monadic type is inferred for the go statement in its current context.

This has the advantage that pure fragments in our monadic sugar can avoid carrying around the rest of the monadic plumbing, even though they use the same bind operator to string it all together.

We can perform similar surgery on the MonadPlus class, tearing it apart into two pieces, breaking out a canonical mzero implementation as a trivial monad that just projects everything to bottom, and having Go erase any lingering mzeros that percolate out of our expression. Rather than reproduce it here, I point to a darcs repository that I just created. You can use darcs to get http://comonad/com/haskell/monad-param or pull the package from hackage. The interesting bits are in Control.Monad.Parameterized and HTML documentation is available.

This package re-exports the MTL and STM monads to avoid the requirement that the end user explicitly import Control.Monad.* masking off the members of Control.Monad each time and it provides some interesting mixins.

Caveat: It appears that GHC enforces the fact that the arguments and results of (>>=) must have a signature like

(>>=) :: forall m a. (...) => m a -> (a -> m b) -> m b

insofar as when you use the do-sugar, your types will not be able to vary. Ideally it should be able to get by with a more liberal signature, but it seems like no one has needed it before now.

]]>
http://comonad.com/reader/2007/parameterized-monads-in-haskell/feed/ 5
Overloaded Functions with Subtyping http://comonad.com/reader/2006/overloaded-functions-with-subtyping/ http://comonad.com/reader/2006/overloaded-functions-with-subtyping/#comments Wed, 01 Nov 2006 08:35:30 +0000 Edward Kmett http://comonad.com/reader/2006/overloaded-functions-with-subtyping/ Was reading Castagna, Ghelli, and Longo's 1995 paper on "A Calculus for Overloaded Functions with Subtyping" today and in it they have to jump through some hoops to index their '&' types to keep them well behaved under β-reduction.

It seems to me, at least from my back-of-the-envelope scribblings, that if you CPS transform the calculus before, that the main technical innovation (overloaded functions using the tighter run-time type information) remains intact, but the need for this technical trick goes away. In this case you know what the reduction will evaluate out to regardless of call-by-value or call-by-need (just bottom), and if the specification changes during evaluation it is still sound, so no need for an index.

 \inference{\Gamma \vdash M:W_1 \leq \lbrace\neg U_i\rbrace_{i\leq(n-1)} & \Gamma \vdash N : W_2 \leq \neg U_n}{\Gamma \vdash (M \binampersand N) : \lbrace \neg U_i \rbrace_{i \leq n }}[$\lbrace\rbrace$-I]

 \inference{\Gamma \vdash M : \lbrace \neg U_i \rbrace_{i \in I} & \Gamma \vdash N : U & U_j = \min_{i \in I} \lbrace U_i \vert U \leq U_i \rbrace } {\Gamma \vdash M \bullet N : \perp }[$\lbrace\rbrace$-E]

The above then would requires explicit continuations and might interfere with rederiving tupling from the overloading mechanism alone, but seems to eliminate some of the barriers they mention to the higher order case. However, I'm not convinced it is a net win regardless, because it would require a notion of typecase.

]]>
http://comonad.com/reader/2006/overloaded-functions-with-subtyping/feed/ 0