-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 List, I'm trying to wrap my head around Haskell and Category Theory---very new to both and in keeping with character, I've jumped into the deep-end. The categories and category-extras packages have helped to illustrate some concepts. However, I remain confused and hope someone can point me in the right direction. The ultimate goal is to construct my own instance of a CCC. Here is the class definition for CCC from the categories package:
class ( Cartesian (<=) , Symmetric (<=) (Product (<=)) , Monoidal (<=) (Product (<=)) ) => CCC (<=) where type Exp (<=) :: * -> * -> * apply :: (Product (<=) (Exp (<=) a b) a) <= b curry :: ((Product (<=) a b) <= c) -> a <= Exp (<=) b c uncurry :: (a <= (Exp (<=) b c)) -> (Product (<=>) a b <= c)
I have the following:
{-# LANGUAGE TypeFamilies, MultiParamTypeClasses, UndecidableInstances #-}
import Control.Category.Braided import Control.Category.Associative import Control.Category.Cartesian import Control.Category.Monoidal import Control.Category.Cartesian.Closed
data MyType a b = MyType {f::(a -> b)} data SomeType a b = SomeType {g::(a,b)}
instance (Symmetric MyType (Product MyType), Monoidal MyType (Product MyType), PreCartesian MyType) => CCC MyType where
type Exp MyType = SomeType
It type checks in ghci and gives the appropriate warnings that apply, curry and uncurry have not been defined---I can't see how to define these. Is it actually possible with the two data types I have? I would really appreciate some help. Lafras -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkyaGWYACgkQKUpCd+bV+kqgWgCfY7B7pUttB0xfeOAN1V3NDqRL fgQAniK/EJsV9jS7XWxmxElCVD6AW0as =l0x/ -----END PGP SIGNATURE-----
On Wed, Sep 22, 2010 at 04:57:42PM +0200, Lafras Uys wrote:
data MyType a b = MyType {f::(a -> b)} data SomeType a b = SomeType {g::(a,b)}
instance (Symmetric MyType (Product MyType), Monoidal MyType (Product MyType), PreCartesian MyType) => CCC MyType where
type Exp MyType = SomeType
This doesn't seem right to me. I would expect type Exp MyType = MyType and type Product MyType = SomeType since the exponential objects corresponding to functions are precisely function types. -Brent
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 01/10/2010 04:54, Brent Yorgey wrote:
On Wed, Sep 22, 2010 at 04:57:42PM +0200, Lafras Uys wrote:
data MyType a b = MyType {f::(a -> b)} data SomeType a b = SomeType {g::(a,b)}
instance (Symmetric MyType (Product MyType), Monoidal MyType (Product MyType), PreCartesian MyType) => CCC MyType where
type Exp MyType = SomeType
This doesn't seem right to me. I would expect
type Exp MyType = MyType
and
type Product MyType = SomeType
since the exponential objects corresponding to functions are precisely function types.
Thanks to everyone who have responded so far, on and off the list. As one person noted, I had to dispense with the class assumptions first. This I've done and everything type checks. It was also suggested that I choose more suggestive names for my data types. Brent, you're right it is not correct. The following seems to work---at least it type checks.
newtype Fun a b = Fun {unFun :: a -> b } newtype Prod a b = Prod {unProd :: (a,b) } deriving (Show)
... class assumptions handled here.
instance (Associative Fun Prod, Disassociative Fun Prod, Symmetric Fun Prod) => PreCartesian Fun where type Product Fun = Prod fst = Fun pFst snd = Fun pSnd diag = Fun pDiag
pApply :: Prod (Fun a b) a -> b pApply (Prod (Fun f, x)) = f x
pCurry :: ((Prod a b) -> c) -> a -> Fun b c pCurry p x = Fun (p . Prod . (,) x)
instance (Symmetric Fun Prod, Monoidal Fun Prod, PreCartesian Fun) => CCC Fun where type Exp Fun = Fun apply = Fun pApply curry (Fun f) = Fun (pCurry f)
I can now find explicit bindings for apply and curry, however not for uncurry. The type signature for uncurry introduces a new type constructor (<=>),
uncurry :: <= a (Exp <= b c) -> <= (Product <=> a b) c
I'm not sure what the meaning of (<=>) is? If someone could provide some pointers, I would be much obliged. Thanks again for all the responses, Lafras -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkylw4UACgkQKUpCd+bV+kr/fACdHnV56mpe3eVoSu91xKdDCaaP +6IAoJVk0Oj+ynJKe7N7io0Y0YA7RBnF =VFkJ -----END PGP SIGNATURE-----
On Fri, Oct 01, 2010 at 01:18:29PM +0200, Lafras Uys wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
I can now find explicit bindings for apply and curry, however not for uncurry. The type signature for uncurry introduces a new type constructor (<=>),
uncurry :: <= a (Exp <= b c) -> <= (Product <=> a b) c
I'm not sure what the meaning of (<=>) is? If someone could provide some pointers, I would be much obliged.
Where did you get these type signatures from? It seems most likely to me that the <=> is just a typo. -Brent
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1 On 02/10/2010 23:35, Brent Yorgey wrote:
On Fri, Oct 01, 2010 at 01:18:29PM +0200, Lafras Uys wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
I can now find explicit bindings for apply and curry, however not for uncurry. The type signature for uncurry introduces a new type constructor (<=>),
uncurry :: <= a (Exp <= b c) -> <= (Product <=> a b) c
I'm not sure what the meaning of (<=>) is? If someone could provide some pointers, I would be much obliged.
Where did you get these type signatures from? It seems most likely to me that the <=> is just a typo.
- From the categories package, http://hackage.haskell.org/package/categories - -- Lafras Uys, Postdoctoral Fellow African Institute for Mathematical Sciences +27 21 787 9349, lafras@aims.ac.za -----BEGIN PGP SIGNATURE----- Version: GnuPG v1.4.10 (GNU/Linux) Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org/ iEYEARECAAYFAkypcyEACgkQKUpCd+bV+krERgCgzgUHXZap3dYUl/Yvmq5KoGZo N7IAn2AM794Yk8qYayHpEwjf48Cadnxh =C0ww -----END PGP SIGNATURE-----
On Mon, Oct 04, 2010 at 08:24:33AM +0200, Lafras Uys wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
On 02/10/2010 23:35, Brent Yorgey wrote:
On Fri, Oct 01, 2010 at 01:18:29PM +0200, Lafras Uys wrote:
-----BEGIN PGP SIGNED MESSAGE----- Hash: SHA1
I can now find explicit bindings for apply and curry, however not for uncurry. The type signature for uncurry introduces a new type constructor (<=>),
uncurry :: <= a (Exp <= b c) -> <= (Product <=> a b) c
I'm not sure what the meaning of (<=>) is? If someone could provide some pointers, I would be much obliged.
Where did you get these type signatures from? It seems most likely to me that the <=> is just a typo.
- From the categories package,
Aha, you're right, it does have (<=>) there, doesn't it? It's definitely a typo. The reason it compiles at all is that (<=>) is just treated as a universally quanitified type variable. But this means it's going to be very difficult to implement uncurry, since you have to yield an arrow from the product of a and b in ANY category, to c. Not only is it impossible to implement, it doesn't even make sense. =) I sent a message to edwardk telling him of the error. In the meantime if you still want to play with this class in the categories package, you can get the source code with cabal unpack categories then edit the code yourself and recompile/install with cabal install in the root of the categories-0.54.1 directory. -Brent
participants (2)
-
Brent Yorgey -
Lafras Uys