Type classes are a language of their own, this is an attempt to document some features.
Work in progress.
Accept values with varying number of arguments
Common technique used in EDSLs (embedded domain-specific languages) to accept functions with varying number of arguments.
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)).
prove from sbv.
prove :: Provable a => a -> IO ThmResult
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
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)
(====) :: Equal a => a -> a -> Property (====) :: (Show a, Arbitrary a, Equal b) => (a -> b) -> (a -> b) -> Property
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).
(,) :: Constraint -> Constraint -> Constraint
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(
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`
class Top x instance Top x
Exists (Show :&: Eq)
data Exists c where Exists :: c a => a -> Exists c
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!(
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 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(
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]
nubEq is slower than
nubOrd, we want to use
nubOrd whenever an
Ord constraint is available and
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
A type is either a constructor (
(->), …) or a type
(->) Int, …). We create a dummy
class with an extra argument which is = 'True when it is an application and
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)
Closed type class
class ClosedTypeClass_ x instance ClosedTypeClass_ Int instance ClosedTypeClass_ Float
type family ClosedTypeClass x :: Constraint where ClosedTypeClass x = ClosedTypeClass_ x
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.
Why the instance resolution doesn’t backtrack.
tweet) Relationship between type classes and logic programming(
reddit) Typeclasses and Run-Time Dependency Management(
Things that are being discussed
#5927) Type level
#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!"