Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Type Classes and Constraints

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.

(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).

Alias for (,) :: Constraint -> Constraint -> Constraint

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 

(blog, reddit) Constraint trick for instances

Uses

Base

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)

Lens

instance (a ~ a', b ~ b') => Each (a, a') (b, b') a b

MagicClasses

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)

Closed type class

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

Things that are being discussed

(#5927) Type level Implies

(#2893) Quantified contexts

(site, reddit) Type classes with arbitrary number of parameters

See also.

(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!"
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment