-----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-----