[Haskell-cafe] Higher order type functions

[Oliver Charles]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160528/efde8fdc/attachment.html>