我可以教 GHC 数学归纳法吗？

Question

我试图创建一个表示无限多类型元组的数据类型：

{-# 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数学归纳法真的没法教吗？

Answer 1

您可以手动包装字典，这样可以懒惰地构建“无限 class 字典”：

{-# 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

我可以教 GHC 数学归纳法吗？

Can I teach GHC mathematical induction?

haskell

tuples

data-kinds