<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<style type="text/css" style="display:none;"><!-- P {margin-top:0;margin-bottom:0;} --></style>
</head>
<body dir="ltr">
<div id="divtagdefaultwrapper" style="font-size:12pt;color:#000000;background-color:#FFFFFF;font-family:Calibri,Arial,Helvetica,sans-serif;">
<p>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?):</p>
<p><br>
</p>
<p>type family NFunctorF f (n :: Nat) a where <br>
  NFunctorF f 0 a = a<br>
  NFunctorF f n a = f (NFunctorF f (n-1) a)<br>
<br>
data MkNFunctor f (n :: Nat) a where<br>
  ZF :: a -> MkNFunctor f 0 a<br>
  SF :: f (MkNFunctor f (n-1) a) -> MkNFunctor f n a<br>
<br>
class NConvertable f (n :: Nat) where<br>
  fromNFunctor :: MkNFunctor f n a -> NFunctorF f n a<br>
  toNFunctor :: NFunctorF f n a -> MkNFunctor f n a<br>
<br>
instance NConvertable f 0 where<br>
  fromNFunctor (ZF x) = x<br>
  toNFunctor x = ZF x<br>
<br>
instance (Functor f, NConvertable f (n-1)) => NConvertable f n where<br>
  fromNFunctor (SF xs) = fmap fromNFunctor xs<br>
  toNFunctor xs = SF (fmap toNFunctor xs)<br>
<br>
type NMaybe = MkNFunctor Maybe<br>
type NList = MkNFunctor []</p>
<p><br>
</p>
<p><br>
</p>
<p>With error:</p>
<p><br>
</p>
<p>    Couldn't match expected type `f (NFunctorF f (n - 1) a)'<br>
                with actual type `NFunctorF f n a'</p>
<p><br>
</p>
<p><br>
</p>
<p>Whereas this happily succeeds.<br>
</p>
<p><br>
</p>
<p>type family NFunctorF f (n :: Peano) a where <br>
  NFunctorF f Zero a = a<br>
  NFunctorF f (Succ n) a = f (NFunctorF f n a)<br>
<br>
data MkNFunctor f (n :: Peano) a where<br>
  ZF :: a -> MkNFunctor f Zero a<br>
  SF :: f (MkNFunctor f n a) -> MkNFunctor f (Succ n) a<br>
<br>
class NConvertable f (n :: Peano) where<br>
  fromNFunctor :: MkNFunctor f n a -> NFunctorF f n a<br>
  toNFunctor :: NFunctorF f n a -> MkNFunctor f n a<br>
<br>
instance NConvertable f Zero where<br>
  fromNFunctor (ZF x) = x<br>
  toNFunctor x = ZF x<br>
<br>
instance (Functor f, NConvertable f n) => NConvertable f (Succ n) where<br>
  fromNFunctor (SF xs) = fmap fromNFunctor xs<br>
  toNFunctor xs = SF (fmap toNFunctor xs)<br>
<br>
type NMaybe = MkNFunctor Maybe<br>
type NList = MkNFunctor []<br>
</p>
<br>
<br>
<p>Is there any way to fix the first version?<br>
</p>
<br>
<p>Cheers,</p>
<p>Daniel</p>
<p><br>
</p>
<div style="color: rgb(0, 0, 0);">
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Haskell-Cafe <haskell-cafe-bounces@haskell.org> on behalf of Daniel Filonik <d.filonik@hdr.qut.edu.au><br>
<b>Sent:</b> Monday, March 7, 2016 5:53 PM<br>
<b>To:</b> amindfv@gmail.com<br>
<b>Cc:</b> haskell-cafe@haskell.org<br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</font>
<div> </div>
</div>
<div>
<div id="divtagdefaultwrapper" style="font-size:12pt; color:#000000; background-color:#FFFFFF; font-family:Calibri,Arial,Helvetica,sans-serif">
<p>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...<br>
</p>
<p><br>
</p>
<p>FYI, I have cleaned up the example a bit, adding some applicative magic, it now looks like:</p>
<p><br>
</p>
<p>data Person = Person { name :: String, age :: Integer, gender :: String, status  :: String } deriving Show<br>
<br>
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<br>
<br>
</p>
<p>persons <$$> groupby (gender) <$$> orderby (age) <$$> select (age + 1) <$$> reduce (sum)<br>
</p>
<p>-- [21,36]<br>
</p>
<p><br>
</p>
<p>Or, if you are feeling more <span>adventurous</span>, you can do thing like:</p>
<p><br>
</p>
<p>let abg = persons <$$> groupby (gender) <$$> select (age) in ((/) <$> (abg <$$> select(realToFrac)) <***> (abg <$$> reduce(mean)))<br>
[[1.0],[1.0588235294117647,0.9411764705882353]]<br>
</p>
<p><br>
</p>
<p>All operations select/reduce/produce/filterby/orderby/groupby work on arbitrarily nested lists, making this very composable.</p>
<p><br>
</p>
<p>Cheers,</p>
<p>Daniel<br>
</p>
<p><br>
</p>
<div style="color:rgb(0,0,0)">
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Daniel Filonik<br>
<b>Sent:</b> Monday, March 7, 2016 3:13 AM<br>
<b>To:</b> amindfv@gmail.com<br>
<b>Cc:</b> haskell-cafe@haskell.org<br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</font>
<div> </div>
</div>
<div>
<div id="divtagdefaultwrapper" style="font-size:12pt; color:#000000; background-color:#FFFFFF; font-family:Calibri,Arial,Helvetica,sans-serif">
<p>I started out using TypeLits, but I was running into problems with GHC's solver along these lines:<br>
</p>
<p><br>
</p>
<p><a title="Ctrl+Click or tap to follow the link" id="LPlnk987751" href="http://stackoverflow.com/questions/24734704/append-for-type-level-numbered-lists-with-typelits">http://stackoverflow.com/questions/24734704/append-for-type-level-numbered-lists-with-typelits</a><br>
</p>
<p><br>
</p>
<p>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!</p>
<p><br>
</p>
<p>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):<br>
</p>
<p><br>
</p>
<p>class NFunctor t (m :: Peano) (n :: Peano) where<br>
  pmap' :: (t (Succ m) a -> t m b) -> t (Succ n) a -> t n b<br>
  zmap' :: (t m a -> t m b) -> t n a -> t n b<br>
  smap' :: (t m a -> t (Succ m) b) -> t n a -> t (Succ n) b<br>
</p>
<br>
<p>Cheers,</p>
<p>Daniel<br>
</p>
<div style="color:rgb(0,0,0)">
<hr tabindex="-1" style="display:inline-block; width:98%">
<div id="divRplyFwdMsg" dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> amindfv@gmail.com <amindfv@gmail.com><br>
<b>Sent:</b> Monday, March 7, 2016 2:38 AM<br>
<b>To:</b> Daniel Filonik<br>
<b>Cc:</b> haskell-cafe@haskell.org<br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</font>
<div> </div>
</div>
<div>
<div></div>
<div>Interesting! What's the reason you redefine the Piano numbers and hide the import of the ones from GHC. TypeLits?</div>
<div><br>
</div>
<div>Tom</div>
<div><br>
</div>
<div><br>
El 6 mar 2016, a las 07:11, Daniel Filonik <<a href="mailto:d.filonik@hdr.qut.edu.au">d.filonik@hdr.qut.edu.au</a>> escribió:<br>
<br>
</div>
<blockquote type="cite">
<div>
<div id="divtagdefaultwrapper" style="font-size:12pt; color:#000000; background-color:#FFFFFF; font-family:Calibri,Arial,Helvetica,sans-serif">
<p>Hi,</p>
<p><br>
</p>
<p>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:</p>
<p><br>
</p>
<p><a title="Ctrl+Click or tap to follow the link" id="LPlnk383182" href="https://byorgey.wordpress.com/2007/08/16/mapping-over-a-nested-functor/">https://byorgey.wordpress.com/2007/08/16/mapping-over-a-nested-functor/</a></p>
<p><br>
</p>
<p>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:</p>
<p><br>
</p>
<p><span class="pl-k">data</span> <span class="pl-c1">Person</span> <span class="pl-k">
=</span> <span class="pl-c1">Person</span> { name <span class="pl-k">::</span> <span class="pl-c1">
String</span>, age <span class="pl-k">::</span> <span class="pl-c1">Integer</span>, gender
<span class="pl-k">::</span> <span class="pl-c1">String</span>, status <span class="pl-k">
::</span> <span class="pl-c1">String</span> } <span class="pl-k">deriving</span> <span class="pl-c1">
Show</span> <br>
</p>
<p><br>
</p>
<p>let persons <span class="pl-k">=</span> fromList' [<span class="pl-c1">Person</span> {name<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Alice<span class="pl-pds">"</span></span>, age<span class="pl-k">=</span><span class="pl-c1">20</span>,
 gender<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>F<span class="pl-pds">"</span></span>, status<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Good<span class="pl-pds">"</span></span>},
<span class="pl-c1">Person</span> {name<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Bob<span class="pl-pds">"</span></span>, age<span class="pl-k">=</span><span class="pl-c1">18</span>, gender<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>M<span class="pl-pds">"</span></span>,
 status<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Good<span class="pl-pds">"</span></span>},
<span class="pl-c1">Person</span> {name<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Chuck<span class="pl-pds">"</span></span>, age<span class="pl-k">=</span><span class="pl-c1">16</span>, gender<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>M<span class="pl-pds">"</span></span>,
 status<span class="pl-k">=</span><span class="pl-s"><span class="pl-pds">"</span>Bad<span class="pl-pds">"</span></span>}]
<span class="pl-k">::</span> <span class="pl-c1">NList</span> N1 <span class="pl-c1">
Person</span><br>
</p>
<p><br>
</p>
<p>persons `select` age<br>
</p>
<p>-- [20,18,16]</p>
<p><br>
</p>
<p>persons `groupby` gender `select` age</p>
<p>-- [[20],[18,16]]</p>
<p><br>
</p>
<p>persons `groupby` gender `groupby` status `select` age</p>
<p>-- [[[20]],[[18],[16]]]<br>
</p>
<p><br>
</p>
<p>Note that "`select` age" works regardless of nesting depth. You can also append or remove nesting levels:<br>
</p>
<p><br>
</p>
<p></p>
<p>persons `groupby` gender `select` age `produce` (\x -> [0..x])</p>
-- [[[0..20]],[[0..18],[0..16]]]
<p></p>
<p><br>
</p>
<p>persons `groupby` gender `reduce` (sumof age)</p>
<p>-- [20, 34]<br>
</p>
<p><br>
</p>
<p>Would this kind of thing be of interest? The code is here:</p>
<p><br>
</p>
<p><a title="Ctrl+Click or tap to follow the link" id="LPlnk826216" href="https://github.com/filonik/nlists">https://github.com/filonik/nlists</a></p>
<p><br>
</p>
<p>Please feel free to suggest improvements.</p>
<p><br>
</p>
<p>Cheers,</p>
<p>Daniel<br>
</p>
</div>
</div>
</blockquote>
<blockquote type="cite">
<div><span>_______________________________________________</span><br>
<span>Haskell-Cafe mailing list</span><br>
<span><a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a></span><br>
<span><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a></span><br>
</div>
</blockquote>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</body>
</html>