[Haskell-cafe] Higher order type functions

[Alexander Vieth]

Ollie has sent you down the right path. I just want to add these relevant
links

https://www.reddit.com/r/haskell/comments/4354x7/promoting_the_arrow_type/?ref=share&ref_source=link
https://github.com/avieth/type-function

Alex

On Sat, May 28, 2016 at 7:23 AM, Oliver Charles <ollie at ocharles.org.uk>
wrote:

> 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.
>
> Hope this helps, and happy to be corrected by others of I'm sending you
> down the wrong path!
>
> Ollie
>
> On Sat, 28 May 2016, 1:22 a.m. Matt, <parsonsmatt at gmail.com> wrote:
>
>> Hi folks!
>>
>> I'm playing with GHC 8 and have the following type family definend:
>>
>> type family InsertSorted (gt :: k -> k -> Bool) (a :: k) (xs :: [k]) ::
>> [k] where
>>     InsertSorted f a '[] = '[a]
>>     InsertSorted f a (x ': xs) = If (f a x) (x ': InsertSorted f a xs) (a
>> ': x ': xs)
>>
>> With appropriate type functions, I can evaluate this in GHCi with
>> `:kind!` and it does what I want:
>>
>> λ> :kind! InsertSorted GreaterThan One '[Two, Four]
>> InsertSorted GreaterThan One '[Two, Four] :: [Face]
>> = '['One, 'Two, 'Four]
>> λ> :kind! InsertSorted GreaterThan Queen '[Two, Four]
>> InsertSorted GreaterThan Queen '[Two, Four] :: [Face]
>> = '['Two, 'Four, 'Queen]
>>
>> However, I get an error if I try to use this in a type signature. This
>> code:
>>
>> data Deck (b :: [k]) where
>>     Empty :: Deck '[]
>>     (:::) :: CardT s f
>>           -> Deck xs
>>           -> Deck (InsertSorted GreaterThan '(s, f) xs)
>>
>> gives me this error:
>>
>>     • The type family ‘GreaterThan’ should have 2 arguments, but has been
>> given
>> none
>>     • In the definition of data constructor ‘:::’
>>       In the data type declaration for ‘Deck’
>>
>>
>> What's the best way to use higher order type families?
>>
>> Thanks!
>> Matt Parsons
>>
>> Here's the definitions I'm using for the above code:
>>
>> data Face
>>     = One | Two | Three | Four | Five | Six | Seven | Eight | Nine
>>     | Jack | Queen | King
>>     deriving (Eq, Ord, Bounded, Enum)
>>
>> type family FaceOrd (a :: Face) (b :: Face) :: Ordering where
>>     FaceOrd a a = 'EQ
>>     FaceOrd a 'One = 'GT
>>     FaceOrd 'One a = 'LT
>>     FaceOrd a b = FaceOrd (PredFace a) (PredFace b)
>>
>> type family FaceGT (a :: Face) (b :: Face) :: Bool where
>>     FaceGT a b = CompK a b == GT
>>
>> class GtK (a :: k) where
>>     type GreaterThan (a :: k) (b :: k) :: Bool
>>
>> instance GtK (a :: Face) where
>>     type GreaterThan a b = CompK a b == GT
>> _______________________________________________
>> 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/20160528/d6ab6f60/attachment.html>