Suppose that I have defined a list like this:
data List a = Nil | Cons a (List a)
Now I want to make sure a List is only instantiated with a generic type which conforms to a specific type class (e.g. Ord). How can I do this?
I know it is possible to define type class constraint on a generic function which is going to work with List instances but is there a way to define such a constraint on the data type itself?
A GADT can capture a dictionary for a constraint in a constructor.
{-# LANGUAGE GADTs #-}
data Sortable a where
Sortable :: Ord a => [a] -> Sortable a
-- ^ ^
-- constructor |
-- |
-- captures an Ord dictionary
The dictionary is reintroduced when you pattern match on the constructor
sortSortable :: Sortable a -> Sortable a
sortSortable (Sortable xs) = Sortable (sort xs)
-- ^ ^
-- match constructor |
-- |
-- reintroduces `Ord a` dictionary so it can be used in sort
Sortable a can be constructed when a has an Ord a instance
{-# LANGUAGE StandaloneDeriving #-}
deriving instance Show a => Show (Sortable a)
main = print . sortSortable $ Sortable "Hello, world!"
But not when it doesn't
data Z = Z
deriving (Show)
main = print . sortSortable $ Sortable [Z]
This results in an error because Sortable can't capture an Ord Z dictionary, because one doesn't exist.
No instance for (Ord Z) arising from a use of ‘Sortable’
In the second argument of ‘($)’, namely ‘Sortable [Z]’
In the expression: print . sortSortable $ Sortable [Z]
In an equation for ‘main’:
main = print . sortSortable $ Sortable [Z]
