CODEWITHSUNDEEP
haskell
nicolas
nicolas

Reputation: 9805

Pattern synonym directionality

The two types are isomorphic, but there is a slight restriction to only unidirectional type synonym for ZeroF for which I am not sure there is a way out of.

data NatF x  = NatF { unNatF :: (forall u. Either u x) }
pattern ZeroF  <- NatF (Left _)
pattern SuccF n = NatF (Right n)

data PeanoF x =  ZeroFP | SuccFP x  -- isomorphe

Am I doing something wrong (beside the contrived example.. ) ?

Upvotes: 0

Views: 69

Answers (1)

Benjamin Hodgson
Benjamin Hodgson

Reputation: 44634

You're having trouble because you've set up your assumptions wrong. forall u. Either u x is not isomorphic to your PeanoF x. The latter is isomorphic to Either () x (or just Maybe x); the former is isomorphic to x.

newtype NatF x = NatF (Maybe x)
pattern ZeroF = NatF Nothing
pattern SuccF n = NatF (Just n)

Upvotes: 4

Related Questions