我目前在进行类型级编程时很有趣。考虑以下版本的链表

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

我想知道是否可以定义一个extendsa的函数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

我想出了不同的方法，迟早都会陷入困境……这是其中两种：

递归方法

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

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。