Nobody has an idea on how to make the TypeLits version work?
Cheers,
Daniel
From: Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of Daniel Filonik <d.filonik@hdr.qut.edu.au>
Sent: Wednesday, March 9, 2016 7:34 AM
To: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] GADTs and Exponentiated FunctorsI have managed to pinpoint where my problems with GHC TypeLits came about. The following fails (btw. are there any guidelines for posting code on this mailing list?):
type family NFunctorF f (n :: Nat) a where
NFunctorF f 0 a = a
NFunctorF f n a = f (NFunctorF f (n-1) a)
data MkNFunctor f (n :: Nat) a where
ZF :: a -> MkNFunctor f 0 a
SF :: f (MkNFunctor f (n-1) a) -> MkNFunctor f n a
class NConvertable f (n :: Nat) where
fromNFunctor :: MkNFunctor f n a -> NFunctorF f n a
toNFunctor :: NFunctorF f n a -> MkNFunctor f n a
instance NConvertable f 0 where
fromNFunctor (ZF x) = x
toNFunctor x = ZF x
instance (Functor f, NConvertable f (n-1)) => NConvertable f n where
fromNFunctor (SF xs) = fmap fromNFunctor xs
toNFunctor xs = SF (fmap toNFunctor xs)
type NMaybe = MkNFunctor Maybe
type NList = MkNFunctor []
With error:
Couldn't match expected type `f (NFunctorF f (n - 1) a)'
with actual type `NFunctorF f n a'
Whereas this happily succeeds.
type family NFunctorF f (n :: Peano) a where
NFunctorF f Zero a = a
NFunctorF f (Succ n) a = f (NFunctorF f n a)
data MkNFunctor f (n :: Peano) a where
ZF :: a -> MkNFunctor f Zero a
SF :: f (MkNFunctor f n a) -> MkNFunctor f (Succ n) a
class NConvertable f (n :: Peano) where
fromNFunctor :: MkNFunctor f n a -> NFunctorF f n a
toNFunctor :: NFunctorF f n a -> MkNFunctor f n a
instance NConvertable f Zero where
fromNFunctor (ZF x) = x
toNFunctor x = ZF x
instance (Functor f, NConvertable f n) => NConvertable f (Succ n) where
fromNFunctor (SF xs) = fmap fromNFunctor xs
toNFunctor xs = SF (fmap toNFunctor xs)
type NMaybe = MkNFunctor Maybe
type NList = MkNFunctor []
Is there any way to fix the first version?
Cheers,
Daniel
From: Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of Daniel Filonik <d.filonik@hdr.qut.edu.au>
Sent: Monday, March 7, 2016 5:53 PM
To: amindfv@gmail.com
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] GADTs and Exponentiated FunctorsJust a quick follow up to this, unless I am mistaken GHC TypeLits does not actually export constructors (Zero, Succ) for the Nat kind, does it? If it did that, of course I could just use those...
FYI, I have cleaned up the example a bit, adding some applicative magic, it now looks like:
data Person = Person { name :: String, age :: Integer, gender :: String, status :: String } deriving Show
persons = fromList' [Person {name="Alice", age=20, gender="F", status="Good"}, Person {name="Bob", age=18, gender="M", status="Good"}, Person {name="Chuck", age=16, gender="M", status="Bad"}] :: NList N1 Person
persons <$$> groupby (gender) <$$> orderby (age) <$$> select (age + 1) <$$> reduce (sum)
-- [21,36]
Or, if you are feeling more adventurous, you can do thing like:
let abg = persons <$$> groupby (gender) <$$> select (age) in ((/) <$> (abg <$$> select(realToFrac)) <***> (abg <$$> reduce(mean)))
[[1.0],[1.0588235294117647,0.9411764705882353]]
All operations select/reduce/produce/filterby/orderby/groupby work on arbitrarily nested lists, making this very composable.
Cheers,
Daniel
From: Daniel Filonik
Sent: Monday, March 7, 2016 3:13 AM
To: amindfv@gmail.com
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] GADTs and Exponentiated FunctorsI started out using TypeLits, but I was running into problems with GHC's solver along these lines:
http://stackoverflow.com/questions/24734704/append-for-type-level-numbered-lists-with-typelits
However, I would not rule out the possibility that this was due to misuse my behalf. If you know a way to make it work, that would be exactly the kind of feedback I am looking for!
Also, I'd be curious if it is possible to write an instance of the general NFunctor for NList (which does not require explicit type annotations to work):
class NFunctor t (m :: Peano) (n :: Peano) where
pmap' :: (t (Succ m) a -> t m b) -> t (Succ n) a -> t n b
zmap' :: (t m a -> t m b) -> t n a -> t n b
smap' :: (t m a -> t (Succ m) b) -> t n a -> t (Succ n) b
Cheers,
Daniel
From: amindfv@gmail.com <amindfv@gmail.com>
Sent: Monday, March 7, 2016 2:38 AM
To: Daniel Filonik
Cc: haskell-cafe@haskell.org
Subject: Re: [Haskell-cafe] GADTs and Exponentiated FunctorsInteresting! What's the reason you redefine the Piano numbers and hide the import of the ones from GHC. TypeLits?
Tom
Hi,
I have been recently playing around with GADTs, using them to keep track of how many times a functor has been applied. This provides a solution to what seems to be a long standing problem, summarized here:
https://byorgey.wordpress.com/2007/08/16/mapping-over-a-nested-functor/
If the nesting depth is part of the type, it is possible to apply fmap automatically as needed. This allows you to write fairly elegant expressions like:
data Person = Person { name :: String, age :: Integer, gender :: String, status :: String } deriving Show
let persons = fromList' [Person {name="Alice", age=20, gender="F", status="Good"}, Person {name="Bob", age=18, gender="M", status="Good"}, Person {name="Chuck", age=16, gender="M", status="Bad"}] :: NList N1 Person
persons `select` age
-- [20,18,16]
persons `groupby` gender `select` age
-- [[20],[18,16]]
persons `groupby` gender `groupby` status `select` age
-- [[[20]],[[18],[16]]]
Note that "`select` age" works regardless of nesting depth. You can also append or remove nesting levels:
persons `groupby` gender `select` age `produce` (\x -> [0..x])
-- [[[0..20]],[[0..18],[0..16]]]
persons `groupby` gender `reduce` (sumof age)
-- [20, 34]
Would this kind of thing be of interest? The code is here:
https://github.com/filonik/nlists
Please feel free to suggest improvements.
Cheers,
Daniel
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe