<div dir="ltr"><a href="https://hackage.haskell.org/package/ghc-typelits-natnormalise">https://hackage.haskell.org/package/ghc-typelits-natnormalise</a> can let you get pretty far, though it triggers a lotta rebuilds :) <br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Mar 12, 2016 at 10:53 AM, Daniel Filonik <span dir="ltr"><<a href="mailto:d.filonik@hdr.qut.edu.au" target="_blank">d.filonik@hdr.qut.edu.au</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr">
<div style="font-size:12pt;color:#000000;background-color:#ffffff;font-family:Calibri,Arial,Helvetica,sans-serif">
<p>Nobody has an idea on how to make the TypeLits version work?<br>
</p>
<br>
Cheers,<br>
Daniel<br>
<div style="color:rgb(0,0,0)">
<hr style="display:inline-block;width:98%">
<div dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><span class=""><b>From:</b> Haskell-Cafe <<a href="mailto:haskell-cafe-bounces@haskell.org" target="_blank">haskell-cafe-bounces@haskell.org</a>> on behalf of Daniel Filonik <<a href="mailto:d.filonik@hdr.qut.edu.au" target="_blank">d.filonik@hdr.qut.edu.au</a>><br>
</span><b>Sent:</b> Wednesday, March 9, 2016 7:34 AM<br>
<b>To:</b> <a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a><div><div class="h5"><br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</div></div></font>
<div> </div>
</div><div><div class="h5">
<div>
<div 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 style="display:inline-block;width:98%">
<div dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> Haskell-Cafe <<a href="mailto:haskell-cafe-bounces@haskell.org" target="_blank">haskell-cafe-bounces@haskell.org</a>> on behalf of Daniel Filonik <<a href="mailto:d.filonik@hdr.qut.edu.au" target="_blank">d.filonik@hdr.qut.edu.au</a>><br>
<b>Sent:</b> Monday, March 7, 2016 5:53 PM<br>
<b>To:</b> <a href="mailto:amindfv@gmail.com" target="_blank">amindfv@gmail.com</a><br>
<b>Cc:</b> <a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a><br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</font>
<div> </div>
</div>
<div>
<div 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 style="display:inline-block;width:98%">
<div 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> <a href="mailto:amindfv@gmail.com" target="_blank">amindfv@gmail.com</a><br>
<b>Cc:</b> <a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a><br>
<b>Subject:</b> Re: [Haskell-cafe] GADTs and Exponentiated Functors</font>
<div> </div>
</div>
<div>
<div 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" href="http://stackoverflow.com/questions/24734704/append-for-type-level-numbered-lists-with-typelits" target="_blank">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 style="display:inline-block;width:98%">
<div dir="ltr"><font style="font-size:11pt" face="Calibri, sans-serif" color="#000000"><b>From:</b> <a href="mailto:amindfv@gmail.com" target="_blank">amindfv@gmail.com</a> <<a href="mailto:amindfv@gmail.com" target="_blank">amindfv@gmail.com</a>><br>
<b>Sent:</b> Monday, March 7, 2016 2:38 AM<br>
<b>To:</b> Daniel Filonik<br>
<b>Cc:</b> <a href="mailto:haskell-cafe@haskell.org" target="_blank">haskell-cafe@haskell.org</a><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" target="_blank">d.filonik@hdr.qut.edu.au</a>> escribió:<br>
<br>
</div>
<blockquote type="cite">
<div>
<div 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" href="https://byorgey.wordpress.com/2007/08/16/mapping-over-a-nested-functor/" target="_blank">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>data</span> <span>Person</span> <span>
=</span> <span>Person</span> { name <span>::</span> <span>
String</span>, age <span>::</span> <span>Integer</span>, gender
<span>::</span> <span>String</span>, status <span>
::</span> <span>String</span> } <span>deriving</span> <span>
Show</span> <br>
</p>
<p><br>
</p>
<p>let persons <span>=</span> fromList' [<span>Person</span> {name<span>=</span><span><span>"</span>Alice<span>"</span></span>, age<span>=</span><span>20</span>,
gender<span>=</span><span><span>"</span>F<span>"</span></span>, status<span>=</span><span><span>"</span>Good<span>"</span></span>},
<span>Person</span> {name<span>=</span><span><span>"</span>Bob<span>"</span></span>, age<span>=</span><span>18</span>, gender<span>=</span><span><span>"</span>M<span>"</span></span>,
status<span>=</span><span><span>"</span>Good<span>"</span></span>},
<span>Person</span> {name<span>=</span><span><span>"</span>Chuck<span>"</span></span>, age<span>=</span><span>16</span>, gender<span>=</span><span><span>"</span>M<span>"</span></span>,
status<span>=</span><span><span>"</span>Bad<span>"</span></span>}]
<span>::</span> <span>NList</span> N1 <span>
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" href="https://github.com/filonik/nlists" target="_blank">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" target="_blank">Haskell-Cafe@haskell.org</a></span><br>
<span><a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a></span><br>
</div>
</blockquote>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div>
</div></div></div>
</div>
</div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org">Haskell-Cafe@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
<br></blockquote></div><br></div>