パターンシノニムの方向性

2つのタイプは同形ですが、単なる単方向のの同義語ZeroFのためのわずかな制限がありますが、そこから抜ける方法はわかりません。パターンシノニムの方向性

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

私は間違ったことを行っていますか？

出典

2017-01-07 nicolas

「u」の定量化は何ですか？これは一般的に有用ではありません。 –

'forall u型のボトムフリーの値は唯一です。どちらかが「何か」という形式のものです。他の方向では、 'ZeroF'は' NatF $ Left undefined'と評価されるべきです。（なぜあなたはそれを使用していますか？） – chi

私は代数F X = 1 + Xを表現したいと思いましたが、明らかにそれはEither（）xです。 – nicolas

仮定が間違っているため、問題が発生しています。 forall u. Either u xはPeanoF xと同形ではありません。後者はEither() x（またはちょうどMaybe x）と同形です。前者はxと同形です。

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

出典

2017-01-08 00:51:57

パターンシノニムの方向性

答えて

関連する問題