dmjio
8/20/2016 - 3:52 PM
Type Classes and Constraints
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.
** ([[https://hackage.haskell.org/package/QuickCheck][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))=.
** ([[https://hackage.haskell.org/package/sbv][Hackage]]) =sbv=
[[https://hackage.haskell.org/package/sbv-5.12/docs/Data-SBV.html#v:prove][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
** ([[https://github.com/Feldspar/feldspar-language/blob/74c29a7a5446915f91c5ec4126f4964ee56d893b/src/Feldspar/Core/Frontend.hs#L316][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
** ([[https://github.com/AccelerateHS/accelerate/blob/179fb230a6af1aa10789c96c1d9be45a2f627b13/Data/Array/Accelerate/Trafo/Vectorise.hs#L2285][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
* ([[https://ghc.haskell.org/trac/ghc/ticket/11523][#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
** ([[https://hackage.haskell.org/package/exists-0.2/docs/Control-Constraint-Combine.html][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 [[http://stackoverflow.com/questions/36964664/haskell-combine-multiple-typeclass-constraints][Haskell combine multiple typeclass constraints]], [[https://hackage.haskell.org/package/generics-sop-0.2.2.0/docs/src/Generics-SOP-Constraint.html#Compose][generics-sop]].
** ([[https://hackage.haskell.org/package/type-operators-0.1.0.3/docs/Control-Type-Operator.html][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)
* ([[https://hackage.haskell.org/package/constraints][Hackage]]) No instances allowed!
From [[https://github.com/ekmett/constraints/blob/master/src/Data/Constraint.hs#L327][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
* ([[http://chrisdone.com/posts/haskell-constraint-trick][blog]], [[https://www.reddit.com/r/haskell/comments/3afi3t/the_constraint_trick_for_instances/][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
*** [[https://ghc.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields/MagicClasses][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
* ([[https://github.com/mikeizbicki/ifcxt][github]]) Constraint level /if/
[[http://chrisdone.com:10001/browse/haskell/?id=21383554×tamp=1441590348#t1441590348][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
* ([[https://hackage.haskell.org/package/constraints-0.8/docs/Data-Constraint-Deferrable.html][Hackage]]) Transform static errors into dynamic checks (Deferrable)
Originally from [[http://people.seas.harvard.edu/~pbuiras/publications/icfp2015.pdf][HLIO: Mixing Static and Dynamic Typing
for Information-Flow Control in Haskell]] which includes examples of use.
* ([[https://mail.haskell.org/pipermail/glasgow-haskell-users/2016-April/026185.html][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: [[https://www.reddit.com/r/haskell/comments/4qqz89/overlappinginstances_workarounds/][OverlappingInstances workarounds]]
** ([[https://gist.github.com/goldfirere/846c3faf7640e27025f0#file-basics-hs-L183][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.
* ([[https://twitter.com/ezyang/status/750364746252165120][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.
* ([[https://www.reddit.com/r/haskell/comments/3afi3t/the_constraint_trick_for_instances/cscb33j][reddit]]) Backtracking
Why the instance resolution doesn't backtrack.
* ([[https://twitter.com/ezyang/status/751570379332804608][tweet]]) Relationship between type classes and logic programming
* ([[https://www.reddit.com/r/haskell/comments/4t089y/typeclasses_and_runtime_dependency_management/][reddit]]) Typeclasses and Run-Time Dependency Management
* Things that are being discussed
** ([[https://ghc.haskell.org/trac/ghc/ticket/5927][#5927]]) Type level =Implies=
** ([[https://ghc.haskell.org/trac/ghc/ticket/2893][#2893]]) Quantified contexts
* ([[https://csks.wordpress.com/2012/10/17/redshift-phase-2-types-classes-for-types-with-arbitrary-numbers-of-parameters/][site]], [[https://www.reddit.com/r/haskell/comments/11nj47/a_class_that_generalizes_over_functor_functor2/][reddit]]) Type classes with arbitrary number of parameters
[[https://gist.github.com/phadej/2fc066c00e33b9486e1a3e5f7767a8d7][See also]].
*** ([[https://gist.github.com/phadej/29335981507d81b4b2f219961772de25][github]]) Existential constraints
** ([[https://downloads.haskell.org/~ghc/8.0.1/docs/html/users_guide/glasgow_exts.html#constraints-in-kinds][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!"