[Haskell-cafe] Higher order type functions

[Matt]

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