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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe