Type classes are a language of their own, this is an attempt to document some features.
Work in progress.
(hackage) reflection
reddit: “With reflection you can make up instances on the fly, but still reason about the resulting types and not lose coherence.”
Provides functions that take type class methods (mappend / mempty) as arguments:
foldBy :: Foldable t => (m -> m -> m) -> m -> t m -> m foldMapBy :: Foldable t => (m -> m -> m) -> m -> (a -> m) -> t a -> m
We recover fold, foldMap by supplying the Monoid methods explicitly:
fold :: (Monoid m, Foldable t) => t m -> m fold = foldBy mappend mempty
foldMap :: (Monoid m, Foldable t) => (a -> m) -> t a -> m foldMap = foldMapBy mappend mempty
Same with traverse where we supply the Applicative methods (pure, <*>) (don’t worry about the scary types):
traverseBy :: Traversable t => (forall x. x -> f x) -> (forall x y. f (x -> y) -> f x -> f y) -> (a -> f b) -> t a -> f (t b) sequenceBy :: Traversable t => (forall x. x -> f x) -> (forall x y. f (x -> y) -> f x -> f y) -> t (f a) -> f (t a)
We recover traverse, sequenceA by supplying the Applicative methods explicitly:
traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse = traverseBy pure (<*>)
sequenceA :: (Traversable t, Applicative f) => t (f a) -> f (t a) sequenceA = sequenceBy pure (<*>)
This shows how to do this for more types: Reflecting values to types and back
Making instances of functions, hardly a trick but may be interesting:
instance Monoid b => Monoid (a -> b)
effectively defines mempty = pure mempty and mappend = liftA2 mappend. Let’s be explicit with types using visible type application TypeApplications:
mempty @(a -> b) = pure @((->) _) (mempty @b) mappend @(a -> b) = liftA2 @((->) _) (mappend @b)
means that mempty has the following types (this can be written mempty, mempty @(_ -> _) and mempty @(_ -> _ -> _))
mempty :: Monoid a => a
mempty :: Monoid b => a -> b mempty _ = mempty
mempty :: Monoid c => a -> b -> c mempty _ _ = mempty
and mappend
mappend :: Monoid a => a -> a -> a mappend a b = mappend a b
mappend :: Monoid b => (a -> b) -> (a -> b) -> (a -> b) (mappend f g) x = mappend (f x) (g x)
mappend :: Monoid c => (a -> b -> c) -> (a -> b -> c) -> (a -> b -> c) (mappend f g) x y = mappend (f x y) (g x y)
These last two may be clearer when written infix (<>) = mappend
(f <> g) x = f x <> g x (f <> g) x y = f x y <> g x y
instance Num a => Num (Maybe a) where (+) = liftA2 (+) (-) = liftA2 (-) (*) = liftA2 (*) abs = fmap abs signum = fmap signum negate = fmap negate fromInteger = pure . fromInteger
Because Applicative ((->) a) this includes making functions numbers:
instance Num b => Num (a -> b) where (+) = liftA2 (+) (-) = liftA2 (-) (*) = liftA2 (*) abs = fmap abs signum = fmap signum negate = fmap negate fromInteger = pure . fromInteger
(github) Subhask
Used heavily in subhask, simplified code:
instance Eq b => Eq (a -> b) where type Logic (a -> b) = a -> Logic b (==) :: (a -> b) -> (a -> b) -> (a -> Logic b) (f == g) a = f a == g a
instance POrd b => POrd (a -> b) where (inf f g) a = inf (f a) (g a)
instance MinBound b => MinBound (a -> b) where (minBound) _ = minBound
instance Lattice b => Lattice (a -> b) where (sup f g) a = sup (f a) (g a)
instance Bounded b => Bounded (a -> b) where (maxBound) _ = maxBound
instance Complemented b => Complemented (a -> b) where (not f) a = not (f a)
instance Heyting b => Heyting (a -> b) where (f ==> g) a = f a ==> g a
instance Boolean b => Boolean (a -> b)
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). This wouldn’t be needed if * and Constraint are made the same. See Class Alias Proposal and its reddit discussion.
“
type Applicative f => (Pointed f, Apply f)
is strictly less useful than
class (Pointed f, Apply f) => Applicative f instance (Pointed f, Apply f) => Applicative f
the latter can be partially applied which is very important once you start using ConstraintKinds in anger and the former requires an extension to be turned on at the use site.”
Also mentioned in this Reddit thread:
“Can’t you do exactly this with constraint kinds?
{-# LANGUAGE ConstraintKinds #-}
type MyClass t a = (Monad t, Monoid (t a))
f :: MyClass t a => a -> a -> t a
f x y = return x `mappend` return y
“
“Or with UndecidableInstances instead of ConstraintKinds:
class (Monad t, Monoid (t a)) => MyClass t a instance (Monad t, Monoid (t a)) => MyClass t a
“
“This has the benefit of
a.) not requiring the end user to turn on an extension and
b.) letting you talk about MyClass :: (* -> *) -> * -> Constraint without having to apply it to type arguments.
Between those two advantages I can’t bring myself to ever use a Constraint-kinded type synonym.”
reddit thread about when this matters.
(#9838) History
“These sorts of synonyms are actually quite common, I think I first used it back around 2006 when I first found haskell: e.g. TXOr in http://hackage.haskell.org/package/type-int-0.5.0.2/docs/src/Data-Type-Boolean.html#TXOr is an instance of this pattern, but it was a well known pattern long before the time I started using it.
The former requires “scarier” extensions than the latter for the person constructing it, but the latter requires an extension to be turned on by the user, hoisting the library designer upon the horns of a dilemma, do they take the burden upon themselves and use “the old way” of thinking about these things or do they make every user turn on `ConstraintKinds`?”
(gihub) Heavily used in the Hask library
FunctorOf which allows it to be made the object constraint for the functor category:
class (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f instance (Functor f, Dom f ~ p, Cod f ~ q) => FunctorOf p q f
and ProductOb which allows it to be made the object constraint for product categories:
class (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j)) instance (Ob p (Fst a), Ob q (Snd a)) => ProductOb (p :: i -> i -> *) (q :: j -> j -> *) (a :: (i,j))
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
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 nubEq
(reddit) Horrible horrible solution
“And if you’re willing to pass in a witness as an argument, you can also use ekmett’s constraints package.” Example:
import Data.Constraint show' :: (Maybe (Dict (Show a))) -> a -> String show' (Just Dict) x = show x show' Nothing _ = "<<not showable>>" t1 = show' (Just Dict) 5 -- "5" t2 = show' Nothing id -- "<<not showable>>" -- Doesn't typecheck -- t3 = show' (Just Dict) id
“Actually, with defer-type-errors you don’t even need the witness!” Example:
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# OPTIONS_GHC -fdefer-type-errors #-}
module Main where
import Data.Constraint
import Control.Exception
import System.IO.Unsafe
show' y = unsafePerformIO $ do
res <- try $ evaluate $ show'' Dict y
case res of
Right x -> return x
Left (ErrorCall _) -> return "no show"
show'' :: (Dict (Show a)) -> a -> String
show'' Dict x = show x
t1 = show' 5
-- "5"
t2 = show' id
-- "no show"
See also Deferrable.
(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
(#7543) Pie in sky: Constraints in type synonyms
This is not a feature, quoting Edward:
“More pie-in-the-sky would be being able to use
type Foo a b = Bar a => Baz a b
instance Foo a b
as
instance Bar a => Baz a b
it would be consistent with the other uses of type, but Bar a => Baz a b doesn’t (currently) have a sensible kind.”
(github) Existential constraints
(#9115) The kind of (=>)
(reddit) Random philosophy
“I remember asking myself the same question in the context of this function:
{-# LANGUAGE GADTs, ScopedTypeVariables, TypeOperators #-}
import Data.Typeable
mwahaha :: forall a. Typeable a => a -> a
mwahaha a = case eqT :: Maybe (a :~: String) of
Just Refl -> "mwahaha!!!"
Nothing -> a
The answer I came up with for myself was based on the logical concepts of contingent vs. tautological truth.
It goes something like this: even though GHC can derive a Typeable instance for any type, that’s however only contingently true. Haskell’s type system is compatible with that circumstance, but also with its negation. So even if it is true that every type is Typeable you still need to appeal to the Typeable a constraint—an “extralogical premise” (so to speak)—in order to write this function.
In contrast, (\a -> a) :: a -> a is just an inevitable consequence of the the way the type system works. So there’s no need to appeal to an “extralogical” constraint. And then that’s what parametricity is about.”
(github) Or, And for constraints
From servant:
If either a or b produce an empty constraint, produce an empty constraint. This works because of coincident overlap within a closed type family:
type family Or (a :: Constraint) (b :: Constraint) :: Constraint where Or () b = () Or a () = ()
If both a or b produce an empty constraint, produce an empty constraint.
type family And (a :: Constraint) (b :: Constraint) :: Constraint where And () () = ()
(reddit) You can write Show a => Read a => a -> a instead of (Show a, Read a) => a -> a
goldfire
“I will close, but your post made me realize something. Instead of writing (Eq a, Show a, Read a) => a -> a, I can write Eq a => Show a => Read a => a -> a, which I somehow like more. Haven’t checked how it Haddocks, though…”
ekmett “goldfire:
Note: the latter is slightly weaker, since in Eq a => Show a => Read a => .. you can only reference backwards up the chain.”
(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!"