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