<div dir="ltr">Fantastic, thanks so much!</div><div class="gmail_extra"><br clear="all"><div><div class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><div>Matt Parsons</div></div></div></div>
<br><div class="gmail_quote">On Sat, May 28, 2016 at 10:00 AM, Alexander Vieth <span dir="ltr"><<a href="mailto:aovieth@gmail.com" target="_blank">aovieth@gmail.com</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">Ollie has sent you down the right path. I just want to add these relevant links<div><br></div><div><a href="https://www.reddit.com/r/haskell/comments/4354x7/promoting_the_arrow_type/?ref=share&ref_source=link" target="_blank">https://www.reddit.com/r/haskell/comments/4354x7/promoting_the_arrow_type/?ref=share&ref_source=link</a><br></div><div><a href="https://github.com/avieth/type-function" target="_blank">https://github.com/avieth/type-function</a></div><div><br><div>Alex</div></div></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Sat, May 28, 2016 at 7:23 AM, Oliver Charles <span dir="ltr"><<a href="mailto:ollie@ocharles.org.uk" target="_blank">ollie@ocharles.org.uk</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><p dir="ltr">I believe that in order to pass around this partially-applied GreaterThan symbol you're going to need to use defunctionalisation. Richard Eisenberg has a blog post on this ("defunctionalisation for the win") which should get you on the right track.</p>
<p dir="ltr">Hope this helps, and happy to be corrected by others of I'm sending you down the wrong path!</p>
<p dir="ltr">Ollie </p>
<br><div class="gmail_quote"><div><div><div dir="ltr">On Sat, 28 May 2016, 1:22 a.m. Matt, <<a href="mailto:parsonsmatt@gmail.com" target="_blank">parsonsmatt@gmail.com</a>> wrote:<br></div></div></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div><div dir="ltr">Hi folks!<div><br></div><div>I'm playing with GHC 8 and have the following type family definend:</div><div><br></div><div><div style="font-family:monospace,monospace">type family InsertSorted (gt :: k -> k -> Bool) (a :: k) (xs :: [k]) :: [k] where</div><div style="font-family:monospace,monospace"> InsertSorted f a '[] = '[a]</div><div style="font-family:monospace,monospace"> InsertSorted f a (x ': xs) = If (f a x) (x ': InsertSorted f a xs) (a ': x ': xs)</div><div style="font-family:monospace,monospace"><br></div><div><font face="arial, helvetica, sans-serif">With appropriate type functions, I can evaluate this in GHCi with `:kind!` and it does what I want:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><font face="monospace, monospace">λ> :kind! InsertSorted GreaterThan One '[Two, Four]</font></div><div><font face="monospace, monospace">InsertSorted GreaterThan One '[Two, Four] :: [Face]</font></div><div><font face="monospace, monospace">= '['One, 'Two, 'Four]</font></div><div><font face="monospace, monospace">λ> :kind! InsertSorted GreaterThan Queen '[Two, Four]</font></div><div><font face="monospace, monospace">InsertSorted GreaterThan Queen '[Two, Four] :: [Face]</font></div><div><font face="monospace, monospace">= '['Two, 'Four, 'Queen]</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div><font face="arial, helvetica, sans-serif">However, I get an error if I try to use this in a type signature. This code:</font></div><div><font face="arial, helvetica, sans-serif"><br></font></div><div><div><font face="monospace, monospace">data Deck (b :: [k]) where</font></div><div><font face="monospace, monospace"> Empty :: Deck '[]</font></div><div><font face="monospace, monospace"> (:::) :: CardT s f </font></div><div><font face="monospace, monospace"> -> Deck xs </font></div><div><font face="monospace, monospace"> -> Deck (InsertSorted GreaterThan '(s, f) xs)</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div style="font-family:arial,helvetica,sans-serif">gives me this error:</div><div style="font-family:arial,helvetica,sans-serif"><br></div><div><div><font face="monospace, monospace"> • The type family ‘GreaterThan’ should have 2 arguments, but has been given</font></div><div><font face="monospace, monospace">none</font></div><div><font face="monospace, monospace"> • In the definition of data constructor ‘:::’</font></div><div><font face="monospace, monospace"> In the data type declaration for ‘Deck’</font></div><div style="font-family:arial,helvetica,sans-serif"><br></div></div><div><br>What's the best way to use higher order type families?</div><div><br></div><div>Thanks!</div><div>Matt Parsons</div><div><br></div><div>Here's the definitions I'm using for the above code:</div><div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">data Face </div><div style="font-family:monospace,monospace"> = One | Two | Three | Four | Five | Six | Seven | Eight | Nine </div><div style="font-family:monospace,monospace"> | Jack | Queen | King</div><div style="font-family:monospace,monospace"> deriving (Eq, Ord, Bounded, Enum) </div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">type family FaceOrd (a :: Face) (b :: Face) :: Ordering where</div><div style="font-family:monospace,monospace"> FaceOrd a a = 'EQ</div><div style="font-family:monospace,monospace"> FaceOrd a 'One = 'GT</div><div style="font-family:monospace,monospace"> FaceOrd 'One a = 'LT</div><div style="font-family:monospace,monospace"> FaceOrd a b = FaceOrd (PredFace a) (PredFace b)</div><div style="font-family:monospace,monospace"><br></div><div style="font-family:monospace,monospace">type family FaceGT (a :: Face) (b :: Face) :: Bool where</div><div style="font-family:monospace,monospace"> FaceGT a b = CompK a b == GT</div><div><br><div><font face="monospace, monospace">class GtK (a :: k) where</font></div><div><font face="monospace, monospace"> type GreaterThan (a :: k) (b :: k) :: Bool</font></div><br></div><div style="font-family:monospace,monospace">instance GtK (a :: Face) where</div><div style="font-family:monospace,monospace"> type GreaterThan a b = CompK a b == GT</div></div></div><div>
</div></div></div></div>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">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>
</blockquote></div>
<br>_______________________________________________<br>
Haskell-Cafe mailing list<br>
<a href="mailto:Haskell-Cafe@haskell.org" target="_blank">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>
</div></div></blockquote></div><br></div>