Reputation: 18137
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
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