Type Family equivalent of `Eq`?
Family type with class shows:
As I don't quite understand, this slide shows two ways of implementation Eq
: via a type class or a family type.
I am familiar with class types and thus implemented MyEq
:
class MyEq a where
eq :: a -> a -> Bool
But when I tried to detect the version type family
, it failed to compile:
data Defined = Yes | No
type family IsEq (a :: *) :: Defined
due to:
TypeEq.hs:30:30: error:
• Type constructor ‘Defined’ cannot be used here
(Perhaps you intended to use DataKinds)
• In the kind ‘Defined’
Please explain how to implement the type family
type class version Eq
. Also, it would be helpful to show the implementation of such an instance type family
(if that's even the right word).
source to share
It's pretty neat, glad I came across this. For those interested, here is a slide deck and paper here . This is a common use case for some language extensions.
{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, ConstraintKinds #-}
data Defined = Yes | No
type family IsEq (a :: *) :: Defined
type Eq a = IsEq a ~ Yes
Then the "implementation" of this is instances of type
type instance IsEq () = Yes -- '()' is an instance of 'Eq'
type instance IsEq Int = Yes -- 'Int' is an instance of 'Eq'
type instance IsEq [a] = IsEq a -- '[a]' is an instance of 'Eq' is 'a' is
You can "try" them in GHCi:
ghci> :kind! IsEq [Int]
IsEq [Int] :: Defined
= Yes
But paper and slide deck don't bother too much about actually providing an equality function. (He mentions saving it in the field Yes
.) So why is it interesting if it isn't even ready to provide class methods? Insofar as
- it provides a better mechanism than overlapping classes
- searching backtracking is easier than using typeclasses
- this allows it to crash from the start with a nice error message (coded as a field in the constructor
No
)
source to share
Try adding DataKinds
As a language extension (for example, at the beginning of the file under the "language" pragma), as the error message suggests.
I have not watched the conversation, but iiuc, Defined
just Bool
where it Yes
is True
. So if you include DataKinds you can just use IsEq a ~ 'True
(and the apostrophe before True just means "this is a type").
Some background: what this extension does is "elevate" every value of any algebraic data type (ie, declared with data
, but not GADTs
, iiuc) into its own type; and then elevates each type to its own view ("view" in Haskell is a "type of types"), i.e. not "kind" (pronounced "star star"), which is a common Haskell meaning that exists at runtime.
By the way:
[Bool] :: *
means "collateral list is type". and [] :: * -> *
means that the type constructor for lists is of type "type to type", that is, "after you provide a List for one type, you get a type".
source to share