Linus Oleander
Linus Oleander

Reputation: 18137

Restrict output using Type Families

I've this code for which I'm trying to add a constraint using Haskells Type Families. I want to force the output to always be a flip, is that possible with this code?

{-# LANGUAGE GADTs, TypeFamilies #-}

module TF where

data Even
data Odd

data Coin where
  Up :: Coin
  Down :: Coin

type family Flip n :: *
type instance Flip Even = Odd
type instance Flip Odd = Even

up = Up 
down = Down

flip Up   = Down
flip Down = Up

Upvotes: 0

Views: 74

Answers (1)

effectfully
effectfully

Reputation: 12715

Putting my comment into an answer:

{-# LANGUAGE GADTs, DataKinds, TypeFamilies #-}

data Parity = Even | Odd

data Coin :: Parity -> * where
    Up   :: Coin Even
    Down :: Coin Odd

type family Flip (p :: Parity) :: Parity where
    Flip Even = Odd
    Flip Odd  = Even

flip :: Coin p -> Coin (Flip p)
flip Up   = Down
flip Down = Up

Upvotes: 4

Related Questions