# [Haskell-cafe] Higher order type functions

Matt parsonsmatt at gmail.com
Sat May 28 00:22:13 UTC 2016

```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...