Type classes are a language of their own, this is an attempt to document some features.
Work in progress.
Common technique used in EDSLs (embedded domain-specific languages) to accept functions with varying number of arguments.
(Hackage) QuickCheck
quickCheck :: Testable prop => prop -> IO ()
QuickCheck allows testing values as well as functions of one, two or more arguments:
quickCheck :: Bool -> IO () quickCheck :: (Int -> Bool) -> IO () quickCheck :: (Int -> Int -> Bool) -> IO () quickCheck :: (Int -> Int -> Int -> Bool) -> IO ()
This is enabled by these instances
instance Testable Bool instance (Arbitrary a, Show a, Testable prop) => Testable (a -> prop)
Keep in mind that the type Int -> Int -> Int -> Bool is Int -> (Int -> (Int -> Bool)).
(Hackage) sbv
prove from sbv.
prove :: Provable a => a -> IO ThmResult
has instances
instance Provable SBool instance (SymWord a, Provable p) => Provable (SBV a -> p)
so it can accept symbolic Booleans
prove :: SBool -> IO ThmResult
as well as Haskell functions returning symbolic Booleans
prove :: SymWord a => (SBV a -> SBool) -> IO ThmResult
(github) Feldspar
Test that two function of the same arity have the same semantics
class Equal a where (====) :: a -> a -> Property
instance (Eq a, Show a) => Equal a where (====) :: a -> a -> Property x ==== y = x === y instance (Show a, Arbitrary a, Equal b) => Equal (a -> b) where (====) :: (a -> b) -> (a -> b) -> Property f ==== g = property (\x -> f x ==== g x)
So
(====) :: Equal a => a -> a -> Property (====) :: (Show a, Arbitrary a, Equal b) => (a -> b) -> (a -> b) -> Property
(github) Accelerate
class Afunction f => Convertible f instance Arrays a => Convertible (S.Acc a) instance (Arrays a, Convertible b) => Convertible (S.Acc a -> b)
fromHOAS :: (Convertible f, Kit acc) => f -> AfunctionR acc aenv f
(#11523) Cyclic definition of a class to make constraint alias
class (Foo f, Bar f) => Baz f instance (Foo f, Bar f) => Baz f
that we can partially apply(?) unlike type Baz f = (Foo f, Bar f).
Same as type p & q = ((p :: Constraint), (q :: Constraint)) except it can be partially applied.
class (p, q) => p & q instance (p, q) => p & q
>>> :kind (&) (&) :: Constraint -> Constraint -> Constraint >>> :kind (&) (Eq _) (&) (Eq _) :: Constraint -> Constraint >>> :kind (&) (Eq _) (Ord _) (&) (Eq _) (Ord _) :: Constraint
(Hackage) Combining constraints
Same as type (c :&: d) a = (c a, d a) except it can be partially applied.
class (c a, d a) => (c :&: d) a instance (c a, d a) => (c :&: d) a infixl 7 :&:
type c `And` d = c :&: d infixl 7 `And`
class f (g x) => (f `Compose` g) x instance f (g x) => (f `Compose` g) x infixr 9 `Compose`
(called Empty in exists package)
class Top x instance Top x
This allows Exists (Show :&: Eq)
data Exists c where Exists :: c a => a -> Exists c
See also Haskell combine multiple typeclass constraints, generics-sop.
(Hackage) Mapping constraints
type-operators contains type families for mapping constraints
Show <=> [a, b] = (Show a, Show b)
[Show, Read] <+> a = (Show a, Read a)
(Hackage) No instances allowed!
From Data.Constraint:
import GHC.Exts (Any)
Any inhabits every kind, including Constraint but is uninhabited, making it impossible to define an instance.
class Any => Bottom where no :: a
We cannot define
instance Bottom
instance a ~ () => PrintfType (IO a) instance a ~ () => HPrintfType (IO a) instance a ~ Char => IsString [a] instance a ~ Char => IsString (DList a) instance (a ~ b, Data a) => Data (a :~: b)
instance (a ~ a', b ~ b') => Each (a, a') (b, b') a b
instance t ~ Float => HasField "area" Triangle t where getField _ (Tri b h _) = 0.5 * b * h instance t ~ Float => HasField "area" Circle t where getField _ (Circle r) = pi * r * r
(github) Constraint level if
IRC:
2015-09-07 03:45:48 +0200 <edwardk> so in the end its basically an incredibly easily broken toy solution
If you have two versions of your function
nubEq :: Eq a => [a] -> [a] nubOrd :: Ord a => [a] -> [a]
where nubEq is slower than nubOrd, we want to use nubOrd whenever an Ord constraint is available and nubEq otherwise:
nub :: forall a. (Eq a, IfCxt (Ord a)) => [a] -> [a] nub = ifCxt (Proxy::Proxy (Ord a)) nubOrd nub
(Hackage) Transform static errors into dynamic checks (Deferrable)
Originally from HLIO: Mixing Static and Dynamic Typing for Information-Flow Control in Haskell which includes examples of use.
(mail) Avoid overlapping instances
instance C [Int] instance C [a]
class IsInt a ~ b => CHelper a b instance CHelper Int True instance IsInt a ~ False => CHelper a False
type family IsInt a where IsInt Int = True IsInt a = False
instance CHelper a (IsInt a) => C [a]
See also: OverlappingInstances workarounds
(github) Typeable
A type is either a constructor (Int, Maybe, (->), …) or a type
application (Maybe Int, (->) Int, …). We create a dummy Typeable' =
class with an extra argument which is = 'True when it is an application and False otherwise:
type family CheckPrim a where CheckPrim (_ _) = 'False CheckPrim _ = 'True
class Typeable' a (b :: Bool) where typeRep' :: TypeRep a
instance (Primitive a, TyConAble a) => Typeable' a 'True where typeRep' = TyCon tyCon
instance (Typeable a, Typeable b) => Typeable' (a b) 'False where typeRep' = TyApp typeRep typeRep
We can then define our Typeable that matches Typeable' a 'True when
a is a constructor and Typeable' (a b) 'False when it is an application:
type Typeable a = Typeable' a (CheckPrim a)
class ClosedTypeClass_ x instance ClosedTypeClass_ Int instance ClosedTypeClass_ Float
type family ClosedTypeClass x :: Constraint where ClosedTypeClass x = ClosedTypeClass_ x
Only export ClosedTypeClass, now further instances cannot be added.
(tweet) Type families v. functional dependencies
Edward Kmett @kmett Jul 5
@ezyang Also, it is easy to go from TFs to fundeps, by using silly shim classes / constraint aliases but you can't go back the other way.
(reddit) Backtracking
Why the instance resolution doesn’t backtrack.
(tweet) Relationship between type classes and logic programming
(reddit) Typeclasses and Run-Time Dependency Management
(#5927) Type level Implies
(#2893) Quantified contexts
(github) Existential constraints
(GHC user guide) Constraints in kinds
As kinds and types are the same, kinds can now (with -XTypeInType) contain type constraints. Only equality constraints are currently supported, however. We expect this to extend to other constraints in the future.
Here is an example of a constrained kind:
type family IsTypeLit a where IsTypeLit Nat = 'True IsTypeLit Symbol = 'True IsTypeLit a = 'False
data T :: forall a. (IsTypeLit a ~ 'True) => a -> * where MkNat :: T 42 MkSymbol :: T "Don't panic!"