I 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-l... 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 Sent: Monday, March 7, 2016 2:38 AM To: Daniel Filonik Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] GADTs and Exponentiated Functors Interesting! What's the reason you redefine the Piano numbers and hide the import of the ones from GHC. TypeLits? Tom El 6 mar 2016, a las 07:11, Daniel Filonik mailto:d.filonik@hdr.qut.edu.au> escribió: 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.orgmailto:Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

I 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 on behalf of Daniel Filonik Sent: Monday, March 7, 2016 5:53 PM To: amindfv@gmail.com Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] GADTs and Exponentiated Functors Just 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 Functors I 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-l... 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 Sent: Monday, March 7, 2016 2:38 AM To: Daniel Filonik Cc: haskell-cafe@haskell.org Subject: Re: [Haskell-cafe] GADTs and Exponentiated Functors Interesting! What's the reason you redefine the Piano numbers and hide the import of the ones from GHC. TypeLits? Tom El 6 mar 2016, a las 07:11, Daniel Filonik mailto:d.filonik@hdr.qut.edu.au> escribió: 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.orgmailto:Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

https://hackage.haskell.org/package/ghc-typelits-natnormalise can let you get pretty far, though it triggers a lotta rebuilds :) On Sat, Mar 12, 2016 at 10:53 AM, Daniel Filonik wrote:

Nobody has an idea on how to make the TypeLits version work?

Cheers, Daniel ------------------------------ *From:* Haskell-Cafe on behalf of Daniel Filonik *Sent:* Wednesday, March 9, 2016 7:34 AM *To:* haskell-cafe@haskell.org

*Subject:* Re: [Haskell-cafe] GADTs and Exponentiated Functors

I 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 on behalf of Daniel Filonik *Sent:* Monday, March 7, 2016 5:53 PM *To:* amindfv@gmail.com *Cc:* haskell-cafe@haskell.org *Subject:* Re: [Haskell-cafe] GADTs and Exponentiated Functors

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

I 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-l...

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 *Sent:* Monday, March 7, 2016 2:38 AM *To:* Daniel Filonik *Cc:* haskell-cafe@haskell.org *Subject:* Re: [Haskell-cafe] GADTs and Exponentiated Functors

Interesting! What's the reason you redefine the Piano numbers and hide the import of the ones from GHC. TypeLits?

Tom

El 6 mar 2016, a las 07:11, Daniel Filonik escribió:

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