[Haskell-cafe] GADTs and Exponentiated Functors

Sat Mar 12 18:07:41 UTC 2016

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 <d.filonik at hdr.qut.edu.au>
wrote:

> Nobody has an idea on how to make the TypeLits version work?
>
> Cheers,
> Daniel
> ------------------------------
> *From:* Haskell-Cafe <haskell-cafe-bounces at haskell.org> on behalf of
> Daniel Filonik <d.filonik at hdr.qut.edu.au>
> *Sent:* Wednesday, March 9, 2016 7:34 AM
> *To:* haskell-cafe at 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 <haskell-cafe-bounces at haskell.org> on behalf of
> Daniel Filonik <d.filonik at hdr.qut.edu.au>
> *Sent:* Monday, March 7, 2016 5:53 PM
> *To:* amindfv at gmail.com
> *Cc:* haskell-cafe at 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 at gmail.com
> *Cc:* haskell-cafe at 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-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 at gmail.com <amindfv at gmail.com>
> *Sent:* Monday, March 7, 2016 2:38 AM
> *To:* Daniel Filonik
> *Cc:* haskell-cafe at 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 <d.filonik at 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 at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160312/d21ccb0c/attachment.html>