CODEWITHSUNDEEP
haskell
Kevin Meredith
Kevin Meredith

Reputation: 41909

Type Family Equivalent of `Eq`?

Type Families with Class shows:

enter image description here

As I incompletely understand, this slide shows 2 ways of implementing Eq: via a type class or type family.

I'm familiar with type classes and thus implemented MyEq:

class MyEq a where 
    eq :: a -> a -> Bool

But, when I tried to define the type family version, 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 version of the Eq type class. Also, it'd be helpful, please, to show an implementation of such a type family instance (if that's even the right word).

Upvotes: 3

Views: 308

Answers (2)

Alec
Alec

Reputation: 32309

This is kind of neat, glad to have stumbled across this. For the interested, here is the slide deck and here is the paper. This is a usual case of needing 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 are instances like

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 out at GHCi:

ghci> :kind! IsEq [Int]
IsEq [Int] :: Defined
= Yes

But the paper and slide deck doesn't really worry too much about actually providing an equality function. (It mentions storing it in a field of Yes). So, why is this interesting if it isn't even ready to provide class methods? Because

  • it makes for a better mechanism than overlapping classes
  • backtracking search is easier than with typeclasses
  • it makes it possible to fail early with nice error message (encoded as a field in the No constructor)

Upvotes: 6

sam boosalis
sam boosalis

Reputation: 1977

Try adding DataKinds As a language extension (i.e. to the top of the file under a "language" pragma) as the error message suggests.

I haven't watched the talk, but iiuc, Defined is just Bool, where Yes is True. So if you enable 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 "raise" every value of any algebraic datatypes (i.e. Declared with data, but not GADTs, iiuc) into its own type; and then raises each type into its own kind (a "kind" in Haskell is the "type of types"), i.e. not of "kind *" (pronounced "kind star"), which is the kind of normal Haskell values that exist at runtime.

btw:

[Bool] :: * means that "a list of liens is a type". and [] :: * -> * means that the type constructor for lists has kind "type to type", i.e. "once you give List a single type, you get back a type".

Upvotes: 1

Related Questions