我可以教GHC数学归纳法吗？
我可以教GHC数学归纳法吗？
提问于 2021-08-24 23:13:50
我尝试创建一个表示无限多个类型的元组的数据类型：
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeNats
infixr 5 :!!
data OmegaTuple (t :: Nat -> *) (n :: Nat) = t n :!! OmegaTuple t (n+1)这很好。
我还试图声明无限多个半群的直积：
instance (Semigroup (t n), Semigroup (OmegaTuple t (n+1))) => Semigroup (OmegaTuple t n) where
(x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys然而GHC像这样抱怨：
• Illegal nested constraint ‘Semigroup (OmegaTuple t (n + 1))’
(Use UndecidableInstances to permit this)如果我没理解错的话，使用UndecidableInstances会使GHC陷入无限循环。
另一次尝试：
instance (Semigroup (t n), forall k. Semigroup (t k) => Semigroup (t (k+1))) => Semigroup (OmegaTuple t n) where
(x :!! xs) <> (y :!! ys) = x <> y :!! xs <> ys然后GHC像这样抱怨：
• Illegal type synonym family application ‘k + 1’ in instance:
Semigroup (t (k + 1))教GHC数学归纳法真的不可能吗？
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-08-25 07:43:56
你可以手动包装字典，这样就可以懒洋洋地建立一个“无限类字典”：
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
import Data.Kind (Type)
import GHC.TypeLits
data SemigroupSequence (t :: Nat -> Type) (n :: Nat) where
SemigroupSequence :: Semigroup (t n)
=> SemigroupSequence t (n+1) -> SemigroupSequence t n
class SemigroupFamily t where
semigroupSequence :: SemigroupSequence t 0然后
mappendOmega :: SemigroupSequence t n
-> OmegaTuple t n -> OmegaTuple t n -> OmegaTuple t n
mappendOmega (SemigroupSequence sd') (x :!! xs) (y :!! ys)
= x <> y :!! mappendOmega sd' xs ys
instance (SemigroupFamily t) => Semigroup (OmegaTuple t 0) where
(<>) = mappendOmega semigroupSequence页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/68915039
复制相关文章
相似问题
腾讯云开发者
