[Haskell-cafe] GADTs and Exponentiated Functors

[Daniel Filonik]

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<mailto: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<mailto: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/20160306/54b0ec97/attachment.html>