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

【问题标题】：Can I teach GHC mathematical induction?我可以教 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数学归纳法吗？

【问题讨论】：

如果没有编译器插件，内置的Nat 几乎没用。尝试用data Nat = Z | S Nat 做所有事情，你的生活会更好。
开启UndecidableInstances 不会总是让 GHC 循环。它所做的是禁用 GHC 通常需要的某些条件。这些条件旨在保证约束检查将终止，但没有这些条件并不能保证它不会终止；可以很容易地预先检查是否终止的程序类别小于实际终止的程序类别。而且我相信 GHC 实际上对于约束解析的深度是有限的，所以如果你搞砸了它仍然会出错。这是一个安全的扩展。
@Ben 不过，在这种情况下，给定Semigroup 实例的任何使用站点确实会无限循环。

标签： haskell tuples data-kinds

【解决方案1】：

您可以手动包装字典，从而可以懒惰地构建“无限类字典”：

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

【讨论】：

您也可以将SemigroupSequence 写成OmegaTuple 为data SemigroupIndexed (t :: k -> Type) (n :: k) where SemigroupIndexed :: Semigroup (t n) => SemigroupIndexed t n 和type SemigroupSequence t = OmegaTuple (SemigroupIndexed t)。这太概括为表示约束适用于无限的类型序列。