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