用值填充链表，其中包含有关类型中编码的长度的信息

Question

我目前在进行类型级编程时遇到了一些乐趣。 考虑以下版本的链表

{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

module ExpLinkedList where

import           GHC.TypeLits (Nat, KnownNat , type (-), type (+))
import           Data.Proxy   (Proxy(..))
import           Data.Kind    (Type)
import           Fcf          (TyEq, If, Eval)

data LinkedList (n :: Nat) (a :: Type) where
  Nil  :: LinkedList 0 a
  (:@) :: a -> LinkedList n a -> LinkedList (n + 1) a

infixr 5 :@

someList :: LinkedList 2 String
someList = "test" :@ "list" :@ Nil

我想知道是否可以定义一个 extends 和 LinkedList 的函数？

例如

extend :: forall m n a . LinkedList n a -> a -> LinkedList (n + m) a
extend vec elem = undefined

example :: LinkedList 5 String
example = extend @3 ("foo" :@ "bar" :@ Nil) "hi"
-- could be: "hi" :@ "hi" :@ "hi" :@ "foo" :@ "bar" :@ Nil

我想出了不同的方法，但迟早都会被卡住……这里有两个：

递归方法

在这种方法中，结束条件由重叠的类型类实例编码

class Extend (b :: Nat) where
  ex :: a -> LinkedList n a -> LinkedList (n + b) a

instance {-# OVERLAPPING #-} Extend 0  where
  ex _ vec = vec

instance Extend n where
  ex a vec = nextEx newVec
  --                ^
  --  • Couldn't match type ‘(n1 + 1) + (n - 1)’ with ‘n1 + n’
  --    Expected type: LinkedList (n1 + n) a
  --      Actual type: LinkedList ((n1 + 1) + (n - 1)) a
    where
      newVec = a :@ vec
      nextEx = ex @(n - 1) a

归纳法

type NextElement (n :: Nat) = Just (n - 1)

class BuildHelper (v :: Maybe Nat) (a :: Type) where
  type CNE v a :: Type
  buildNext :: Proxy v -> a -> CNE v a

instance BuildHelper 'Nothing a where
  type CNE 'Nothing a = LinkedList 0 a
  buildNext _ a = Nil

instance BuildHelper ('Just m) a where
  type CNE ('Just m) a = LinkedList (m + 1) a
  buildNext _ a = a :@ buildNext proxy a
--                     ^
-- • Couldn't match expected type ‘LinkedList m a’
--                  with actual type ‘CNE
--                                      (If (TyEq m 0) 'Nothing ('Just (m - 1))) 
    where
      proxy = Proxy @(NextElement m)

用笔和纸评估这个似乎可行

-- buildNext (Proxy @(Just 2) True) :: proxy -> Bool -> Vector 3 Bool
-- = a :@ buildNext @(NextElement 2) a
-- = a :@ buildNext @(Just 1) a
-- = a :@ a :@ buildNext @(NextElement 1) a
-- = a :@ a :@ buildNext @(Just 0) a
-- = a :@ a :@ a :@ buildNext @(NextElement 0) a
-- = a :@ a :@ a :@ buildNext @(Nothing) a
-- = a :@ a :@ a :@ Nil

基本上，GHC 无法证明 m 与 (m - 1) + 1 匹配。

Answer 1

这是单例的典型用例。

此外，此解决方案依赖于算术属性，这些属性在 GHC 的类型检查器中本机不可用，但由 ghc-typelits-natnormalise 插件提供。

Nat 推理插件

具体来说，附加长度索引列表利用(+)的关联性：在m = p + 1的情况下，extend签名中的输出列表类型是LList (n + m) = LList (n + (p + 1))，这需要关联性等于@ 987654329@ 以便可以使用构造函数(:@)。我们还需要可交换性，除非我们在代码和证明中小心谨慎，例如不要混淆1 + p 和p + 1。无论如何，安装该软件包并添加以下行会教 GHC 一些基本算法：

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}  -- from the package ghc-typelits-natnormalise

请注意，我们不必在代码中明确地进行任何此类推理；该插件在类型检查期间为编译器提供知识。

单身人士

函数extend :: forall n m a. a -> LList m a -> LList (n + m) a需要看m的值才能知道要插入多少个as；我们必须更改extend 的类型以提供必要的运行时信息。单例提供了一个通用的解决方案。具体来说，我们可以为Nat 类型定义以下单例类型，它的特点是运行时表示类型为SNat n 的值（即只查看构造函数SZ和SS) 唯一确定索引n：

data SNat (n :: Nat) where
  SZ :: SNat 0
  SS :: SNat n -> SNat (1 + n)

• 另见博文Introduction to singletons。

extend的定义

然后的想法是将签名从extend :: forall n. ... 更改为extend :: SNat n -> ...，增加Nat (forall n) 上的量化，这将在运行时擦除，使用SNat n 参数和具体运行-时间表示。然后可以通过SNat n 参数上的模式匹配来定义该函数：

extend :: SNat n -> a -> LList m a -> LList (n + m) a
extend SZ _ ys = ys
extend (SS n) x ys = x :@ extend n x ys

请注意，如果我们忽略类型，则此定义与使用简单 Peano naturals 的简单列表（未按其长度索引）上的 extend 变体相同。函数extend 是索引类型的众多示例之一，索引类型只是未索引程序的更精确的类型化版本：

-- Peano representation of natural numbers
data PNat where
  Z :: PNat
  S :: PNat -> PNat

-- Non-indexed variant of extend
extendP :: PNat -> a -> [a] -> [a]
extendP Z _ ys = ys
extendP (S n) x ys = x : extendP n x ys

示例

一个使用extend的例子：

example :: LList 5 String
example = extend (SS (SS (SS SZ))) "hi" ("foo" :@ "bar" :@ Nil)

我们必须用一元写数字，这不是很有趣。我们可以使用类型类将 Nat 文字转换为它们的 SNat 单例值。

隐式构造SNat

class ISNat n where
  snat :: SNat n

正如您可能已经预料的那样，将有两个实例，分别用于0 和后继者。 0 是显而易见的：

instance ISNat 0 where
  snat = SZ

对于后继者，术语级别的部分很简单 (snat = SS snat)，但类型需要一些技巧。

instance {-# OVERLAPPABLE #-} (ISNat p, n ~ (1 + p)) => ISNat n where
  snat = SS snat

第一，OVERLAPPABLE。没有简单的方法可以在语法上将类型参数n 标识为“不是0”，因此我们使用OVERLAPPABLE 实例。 （如果重叠不可接受，还有其他方法，但它们不那么方便。）遇到ISNat n 约束时，类型检查器将始终选择最具体的实例：如果n 是0，它将选择@ 987654373@ 实例，如果n 是非零文字，它将选择此可重叠实例作为后继实例，因为0 实例不适用，并且如果n 不等于文字（因此它是无约束的类型变量或一些卡住的类型系列应用程序），0 实例可能适用，我们真的不知道，所以类型检查器保守地不会选择这些实例中的任何一个，而是会在其上下文的其他地方寻找合适的约束，如果没有找到，则会引发编译时错误。

第二，SS 希望其结果类型为SNat (1 + p) 形式。所以我们添加一个约束n ~ (1 + p)。

请注意，要解决该约束（当使用 snat 时），GHC 将需要猜测 p，natnormalise 插件会在这里处理；否则我们也可以添加一个约束p ~ (n - 1)。

这样我们终于可以使用Nat 文字更方便地编写示例：

extend (snat :: SNat 3) "hi" ("foo" :@ "bar" :@ Nil)

snat :: SNat 位可能看起来有点笨拙。留给读者作为练习。

完整要点：https://gist.github.com/Lysxia/cf0f8ae509d36a11ddf58bfcea8abb89