证明 GHC 的类型不等式
Proving a type inequality to GHC
出于教育目的,我一直在尝试通过使用各种语言扩展和单例类型在 Haskell 中重建 "Type-Driven Development with Idris" 一书中的示例(即 RemoveElem.idr)。它的要点是一个从非空向量中删除元素的函数,前提是该元素实际上在向量中。以下代码是自包含的(GHC 8.4 或更高版本)。问题出现在最后:
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
import Data.Type.Equality
import Data.Void
-- | Inductively defined natural numbers.
data Nat = Z | S Nat deriving (Eq, Show)
-- | Singleton types for natural numbers.
data SNat :: Nat -> Type where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
deriving instance Show (SNat n)
-- | "Demote" a singleton-typed natural number to an ordinary 'Nat'.
fromSNat :: SNat n -> Nat
fromSNat SZ = Z
fromSNat (SS n) = S (fromSNat n)
-- | A decidable proposition.
data Dec a = Yes a | No (a -> Void)
-- | Propositional equality of natural numbers.
eqSNat :: SNat a -> SNat b -> Dec (a :~: b)
eqSNat SZ SZ = Yes Refl
eqSNat SZ (SS _) = No (\case {})
eqSNat (SS _) SZ = No (\case {})
eqSNat (SS a) (SS b) = case eqSNat a b of
No f -> No (\case Refl -> f Refl)
Yes Refl -> Yes Refl
-- | A length-indexed list (aka vector).
data Vect :: Nat -> Type -> Type where
Nil :: Vect 'Z a
(:::) :: a -> Vect n a -> Vect ('S n) a
infixr 5 :::
deriving instance Show a => Show (Vect n a)
-- | @Elem a v@ is the proposition that an element of type @a@
-- is contained in a vector of type @v@. To be useful, @a@ and @v@
-- need to refer to singleton types.
data Elem :: forall a n. a -> Vect n a -> Type where
Here :: Elem x (x '::: xs)
There :: Elem x xs -> Elem x (y '::: xs)
deriving instance Show a => Show (Elem a v)
------------------------------------------------------------------------
-- From here on, to simplify things, only vectors of natural
-- numbers are considered.
-- | Singleton types for vectors of 'Nat's.
data SNatVect :: forall n. Nat -> Vect n Nat -> Type where
SNatNil :: SNatVect 'Z 'Nil
SNatCons :: SNat a -> SNatVect n v -> SNatVect ('S n) (a '::: v)
deriving instance Show (SNatVect n v)
-- | "Demote" a singleton-typed vector of 'SNat's to an
-- ordinary vector of 'Nat's.
fromSNatVect :: SNatVect n v -> Vect n Nat
fromSNatVect SNatNil = Nil
fromSNatVect (SNatCons a v) = fromSNat a ::: fromSNatVect v
-- | Decide whether a value is in a vector.
isElem :: SNat a -> SNatVect n v -> Dec (Elem a v)
isElem _ SNatNil = No (\case {})
isElem a (SNatCons b as) = case eqSNat a b of
Yes Refl -> Yes Here
No notHere -> case isElem a as of
Yes there -> Yes (There there)
No notThere -> No $ \case
Here -> notHere Refl
There there -> notThere there
type family RemoveElem (a :: Nat) (v :: Vect ('S n) Nat) :: Vect n Nat where
RemoveElem a (a '::: as) = as
RemoveElem a (b '::: as) = b '::: RemoveElem a as
-- | Remove a (singleton-typed) element from a (non-empty, singleton-typed)
-- vector, given a proof that the element is in the vector.
removeElem :: forall (a :: Nat) (v :: Vect ('S n) Nat)
. SNat a
-> Elem a v
-> SNatVect ('S n) v
-> SNatVect n (RemoveElem a v)
removeElem x prf (SNatCons y ys) = case prf of
Here -> ys
There later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> SNatCons y (removeElem x later ys)
-- ^ Could not deduce:
-- RemoveElem a (y '::: (a2 '::: v2))
-- ~ (y '::: RemoveElem a (a2 '::: v2))
显然,类型系统需要说服值 x
和 y
的类型在代码的那个分支中不可能相等,以便类型族的第二个等式可以明确地用于根据需要减少 return 类型。我不知道该怎么做。天真地,我希望构造函数 There
以及 There later
上的模式匹配携带/揭示 GHC 类型不等式的证明。
以下是一个明显冗余的部分解决方案,它仅演示了 GHC 对递归调用进行类型检查所需的类型不等式:
SNatCons{} -> case (x, y) of
(SZ, SS _) -> SNatCons y (removeElem x later ys)
(SS _, SZ) -> SNatCons y (removeElem x later ys)
现在,例如这有效:
λ> let vec = SNatCons SZ (SNatCons (SS SZ) (SNatCons SZ SNatNil))
λ> :t vec
vec
:: SNatVect ('S ('S ('S 'Z))) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let Yes prf = isElem (SS SZ) vec
λ> :t prf
prf :: Elem ('S 'Z) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let vec' = removeElem (SS SZ) prf vec
λ> :t vec'
vec' :: SNatVect ('S ('S 'Z)) ('Z '::: ('Z '::: 'Nil))
λ> fromSNatVect vec'
Z ::: (Z ::: Nil)
分辨率
正如@chi 的评论中所暗示并在 中详细阐述的那样,我试图通过使用上述类型签名和类型族编写 removeElem
来解决错误的问题,如果我愿意的话能够,生成的程序将是错误类型的。
以下是我根据 HTNW 的回答所做的更正(您可能需要在继续此处之前阅读它)。
第一个错误或不必要的复杂化是在 SNatVect
s 类型中重复向量的长度。我认为有必要写fromSNatVect
,但肯定不是:
data SNatVect (v :: Vect n Nat) :: Type where
SNatNil :: SNatVect 'Nil
SNatCons :: SNat a -> SNatVect v -> SNatVect (a '::: v)
deriving instance Show (SNatVect v)
fromSNatVect :: forall (v :: Vect n Nat). SNatVect v -> Vect n Nat
-- implementation unchanged
现在有两种写法removeElem
。第一个接受 Elem
、SNatVect
和 returns Vect
:
removeElem :: forall (a :: Nat) (n :: Nat) (v :: Vect ('S n) Nat)
. Elem a v
-> SNatVect v
-> Vect n Nat
removeElem prf (SNatCons y ys) = case prf of
Here -> fromSNatVect ys
There later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> fromSNat y ::: removeElem later ys
第二个采用 SElem
、SNatVect
和 return 和 SNatVect
,使用反映值级别的 RemoveElem
类型族功能:
data SElem (e :: Elem a (v :: Vect n k)) where
SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))
type family RemoveElem (xs :: Vect ('S n) a) (e :: Elem x xs) :: Vect n a where
RemoveElem (x '::: xs) 'Here = xs
RemoveElem (x '::: xs) ('There later) = x '::: RemoveElem xs later
sRemoveElem :: forall (xs :: Vect ('S n) Nat) (e :: Elem x xs)
. SElem e
-> SNatVect xs
-> SNatVect (RemoveElem xs e)
sRemoveElem prf (SNatCons y ys) = case prf of
SHere -> ys
SThere later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> SNatCons y (sRemoveElem later ys)
有趣的是,这两个版本都取消了将要删除的元素作为单独的参数传递,因为该信息包含在 Elem
/ SElem
值中。 value
参数也可以从该函数的 Idris 版本中删除,尽管这样 removeElem_auto 变体可能会有点混乱,因为它只会将向量作为显式参数并删除第一个向量的元素,如果隐式 prf
参数未明确用于不同的证明。
考虑[1, 2, 1]
。 RemoveElem 1 [1, 2, 1]
是 [2, 1]
。现在,调用 removeElem 1 (There $ There $ Here) ([1, 2, 1] :: SNatVect 3 [1, 2, 1]) :: SNatVect 2 [2, 1]
应该可以编译。这是错误的。 Elem
参数表示删除第三个元素,这将给出 [1, 2]
,但类型签名表示它必须是 [2, 1]
.
首先,SNatVect
有点破。它有两个 Nat
个参数:
data SNatVect :: forall n. Nat -> Vect n a -> Type where ...
第一个是n
,第二个是未命名的Nat
。通过SNatVect
的结构,它们总是相等的。它允许 SNatVect
加倍作为相等性证明,但它可能不是有意这样做的。你可能是说
data SNatVect (n :: Nat) :: Vect n Nat -> Type where ...
无法仅使用正常的 ->
语法在源代码 Haskell 中编写此签名。但是,当 GHC 打印此类型时,您有时会得到
SNatVect :: forall (n :: Nat) -> Vect n Nat -> Type
但这是多余的。您可以将 Nat
作为隐式 forall
参数,并从 Vect
s 类型中推断出它:
data SNatVect (xs :: Vect n Nat) where
SNatNil :: SNatVect 'Nil
SNatCons :: SNat x -> SNatVect xs -> SNatVect (x '::: xs)
这给了
SNatVect :: forall (n :: Nat). Vect n Nat -> Type
其次,尝试写作
removeElem :: forall (n :: Nat) (x :: Nat) (xs :: Vect (S n) Nat).
Elem x xs -> SNatVect xs -> Vect n Nat
请注意 SNat
参数是如何消失的,以及 return 类型是如何成为一个简单的 Vect
。 SNat
参数生成了 "too big" 类型,所以当函数没有意义时,您会陷入使它有点工作的状态。 SNatVect
return 类型表示您正在跳过步骤。粗略地说,每个函数都有三种形式:基本形式,f :: a -> b -> c
;类型级别的,type family F (x :: a) (y :: b) :: c
;和依赖的,f :: forall (x :: a) (y :: b). Sing x -> Sing y -> Sing (F x y)
。每一个都以 "same" 方式实现,但是试图在不实现其前身的情况下实现一个是肯定会混淆的方式。
现在,你可以稍微提升一下:
data SElem (e :: Elem x (xs :: Vect n k)) where
SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))
type family RemoveElem (xs :: Vect (S n) a) (e :: Elem x xs) :: Vect n a
注意removeElem
和RemoveElem
类型之间的关系。参数的重新排序是因为 e
的类型取决于 xs
,因此需要相应地对它们进行排序。或者:xs
参数从 forall
'd-and-implicitly-given 提升为 explicitly-given,然后 Sing xs
参数被否决,因为它不包含任何信息,由于单身人士。
终于可以写这个函数了:
sRemoveElem :: forall (xs :: Vect (S n) Nat) (e :: Elem x xs).
SElem e -> SNatVect xs -> SNatVect (RemoveElem xs e)
出于教育目的,我一直在尝试通过使用各种语言扩展和单例类型在 Haskell 中重建 "Type-Driven Development with Idris" 一书中的示例(即 RemoveElem.idr)。它的要点是一个从非空向量中删除元素的函数,前提是该元素实际上在向量中。以下代码是自包含的(GHC 8.4 或更高版本)。问题出现在最后:
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
import Data.Kind
import Data.Type.Equality
import Data.Void
-- | Inductively defined natural numbers.
data Nat = Z | S Nat deriving (Eq, Show)
-- | Singleton types for natural numbers.
data SNat :: Nat -> Type where
SZ :: SNat 'Z
SS :: SNat n -> SNat ('S n)
deriving instance Show (SNat n)
-- | "Demote" a singleton-typed natural number to an ordinary 'Nat'.
fromSNat :: SNat n -> Nat
fromSNat SZ = Z
fromSNat (SS n) = S (fromSNat n)
-- | A decidable proposition.
data Dec a = Yes a | No (a -> Void)
-- | Propositional equality of natural numbers.
eqSNat :: SNat a -> SNat b -> Dec (a :~: b)
eqSNat SZ SZ = Yes Refl
eqSNat SZ (SS _) = No (\case {})
eqSNat (SS _) SZ = No (\case {})
eqSNat (SS a) (SS b) = case eqSNat a b of
No f -> No (\case Refl -> f Refl)
Yes Refl -> Yes Refl
-- | A length-indexed list (aka vector).
data Vect :: Nat -> Type -> Type where
Nil :: Vect 'Z a
(:::) :: a -> Vect n a -> Vect ('S n) a
infixr 5 :::
deriving instance Show a => Show (Vect n a)
-- | @Elem a v@ is the proposition that an element of type @a@
-- is contained in a vector of type @v@. To be useful, @a@ and @v@
-- need to refer to singleton types.
data Elem :: forall a n. a -> Vect n a -> Type where
Here :: Elem x (x '::: xs)
There :: Elem x xs -> Elem x (y '::: xs)
deriving instance Show a => Show (Elem a v)
------------------------------------------------------------------------
-- From here on, to simplify things, only vectors of natural
-- numbers are considered.
-- | Singleton types for vectors of 'Nat's.
data SNatVect :: forall n. Nat -> Vect n Nat -> Type where
SNatNil :: SNatVect 'Z 'Nil
SNatCons :: SNat a -> SNatVect n v -> SNatVect ('S n) (a '::: v)
deriving instance Show (SNatVect n v)
-- | "Demote" a singleton-typed vector of 'SNat's to an
-- ordinary vector of 'Nat's.
fromSNatVect :: SNatVect n v -> Vect n Nat
fromSNatVect SNatNil = Nil
fromSNatVect (SNatCons a v) = fromSNat a ::: fromSNatVect v
-- | Decide whether a value is in a vector.
isElem :: SNat a -> SNatVect n v -> Dec (Elem a v)
isElem _ SNatNil = No (\case {})
isElem a (SNatCons b as) = case eqSNat a b of
Yes Refl -> Yes Here
No notHere -> case isElem a as of
Yes there -> Yes (There there)
No notThere -> No $ \case
Here -> notHere Refl
There there -> notThere there
type family RemoveElem (a :: Nat) (v :: Vect ('S n) Nat) :: Vect n Nat where
RemoveElem a (a '::: as) = as
RemoveElem a (b '::: as) = b '::: RemoveElem a as
-- | Remove a (singleton-typed) element from a (non-empty, singleton-typed)
-- vector, given a proof that the element is in the vector.
removeElem :: forall (a :: Nat) (v :: Vect ('S n) Nat)
. SNat a
-> Elem a v
-> SNatVect ('S n) v
-> SNatVect n (RemoveElem a v)
removeElem x prf (SNatCons y ys) = case prf of
Here -> ys
There later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> SNatCons y (removeElem x later ys)
-- ^ Could not deduce:
-- RemoveElem a (y '::: (a2 '::: v2))
-- ~ (y '::: RemoveElem a (a2 '::: v2))
显然,类型系统需要说服值 x
和 y
的类型在代码的那个分支中不可能相等,以便类型族的第二个等式可以明确地用于根据需要减少 return 类型。我不知道该怎么做。天真地,我希望构造函数 There
以及 There later
上的模式匹配携带/揭示 GHC 类型不等式的证明。
以下是一个明显冗余的部分解决方案,它仅演示了 GHC 对递归调用进行类型检查所需的类型不等式:
SNatCons{} -> case (x, y) of
(SZ, SS _) -> SNatCons y (removeElem x later ys)
(SS _, SZ) -> SNatCons y (removeElem x later ys)
现在,例如这有效:
λ> let vec = SNatCons SZ (SNatCons (SS SZ) (SNatCons SZ SNatNil))
λ> :t vec
vec
:: SNatVect ('S ('S ('S 'Z))) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let Yes prf = isElem (SS SZ) vec
λ> :t prf
prf :: Elem ('S 'Z) ('Z '::: ('S 'Z '::: ('Z '::: 'Nil)))
λ> let vec' = removeElem (SS SZ) prf vec
λ> :t vec'
vec' :: SNatVect ('S ('S 'Z)) ('Z '::: ('Z '::: 'Nil))
λ> fromSNatVect vec'
Z ::: (Z ::: Nil)
分辨率
正如@chi 的评论中所暗示并在 removeElem
来解决错误的问题,如果我愿意的话能够,生成的程序将是错误类型的。
以下是我根据 HTNW 的回答所做的更正(您可能需要在继续此处之前阅读它)。
第一个错误或不必要的复杂化是在 SNatVect
s 类型中重复向量的长度。我认为有必要写fromSNatVect
,但肯定不是:
data SNatVect (v :: Vect n Nat) :: Type where
SNatNil :: SNatVect 'Nil
SNatCons :: SNat a -> SNatVect v -> SNatVect (a '::: v)
deriving instance Show (SNatVect v)
fromSNatVect :: forall (v :: Vect n Nat). SNatVect v -> Vect n Nat
-- implementation unchanged
现在有两种写法removeElem
。第一个接受 Elem
、SNatVect
和 returns Vect
:
removeElem :: forall (a :: Nat) (n :: Nat) (v :: Vect ('S n) Nat)
. Elem a v
-> SNatVect v
-> Vect n Nat
removeElem prf (SNatCons y ys) = case prf of
Here -> fromSNatVect ys
There later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> fromSNat y ::: removeElem later ys
第二个采用 SElem
、SNatVect
和 return 和 SNatVect
,使用反映值级别的 RemoveElem
类型族功能:
data SElem (e :: Elem a (v :: Vect n k)) where
SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))
type family RemoveElem (xs :: Vect ('S n) a) (e :: Elem x xs) :: Vect n a where
RemoveElem (x '::: xs) 'Here = xs
RemoveElem (x '::: xs) ('There later) = x '::: RemoveElem xs later
sRemoveElem :: forall (xs :: Vect ('S n) Nat) (e :: Elem x xs)
. SElem e
-> SNatVect xs
-> SNatVect (RemoveElem xs e)
sRemoveElem prf (SNatCons y ys) = case prf of
SHere -> ys
SThere later -> case ys of
SNatNil -> case later of {}
SNatCons{} -> SNatCons y (sRemoveElem later ys)
有趣的是,这两个版本都取消了将要删除的元素作为单独的参数传递,因为该信息包含在 Elem
/ SElem
值中。 value
参数也可以从该函数的 Idris 版本中删除,尽管这样 removeElem_auto 变体可能会有点混乱,因为它只会将向量作为显式参数并删除第一个向量的元素,如果隐式 prf
参数未明确用于不同的证明。
考虑[1, 2, 1]
。 RemoveElem 1 [1, 2, 1]
是 [2, 1]
。现在,调用 removeElem 1 (There $ There $ Here) ([1, 2, 1] :: SNatVect 3 [1, 2, 1]) :: SNatVect 2 [2, 1]
应该可以编译。这是错误的。 Elem
参数表示删除第三个元素,这将给出 [1, 2]
,但类型签名表示它必须是 [2, 1]
.
首先,SNatVect
有点破。它有两个 Nat
个参数:
data SNatVect :: forall n. Nat -> Vect n a -> Type where ...
第一个是n
,第二个是未命名的Nat
。通过SNatVect
的结构,它们总是相等的。它允许 SNatVect
加倍作为相等性证明,但它可能不是有意这样做的。你可能是说
data SNatVect (n :: Nat) :: Vect n Nat -> Type where ...
无法仅使用正常的 ->
语法在源代码 Haskell 中编写此签名。但是,当 GHC 打印此类型时,您有时会得到
SNatVect :: forall (n :: Nat) -> Vect n Nat -> Type
但这是多余的。您可以将 Nat
作为隐式 forall
参数,并从 Vect
s 类型中推断出它:
data SNatVect (xs :: Vect n Nat) where
SNatNil :: SNatVect 'Nil
SNatCons :: SNat x -> SNatVect xs -> SNatVect (x '::: xs)
这给了
SNatVect :: forall (n :: Nat). Vect n Nat -> Type
其次,尝试写作
removeElem :: forall (n :: Nat) (x :: Nat) (xs :: Vect (S n) Nat).
Elem x xs -> SNatVect xs -> Vect n Nat
请注意 SNat
参数是如何消失的,以及 return 类型是如何成为一个简单的 Vect
。 SNat
参数生成了 "too big" 类型,所以当函数没有意义时,您会陷入使它有点工作的状态。 SNatVect
return 类型表示您正在跳过步骤。粗略地说,每个函数都有三种形式:基本形式,f :: a -> b -> c
;类型级别的,type family F (x :: a) (y :: b) :: c
;和依赖的,f :: forall (x :: a) (y :: b). Sing x -> Sing y -> Sing (F x y)
。每一个都以 "same" 方式实现,但是试图在不实现其前身的情况下实现一个是肯定会混淆的方式。
现在,你可以稍微提升一下:
data SElem (e :: Elem x (xs :: Vect n k)) where
SHere :: forall x xs. SElem ('Here :: Elem x (x '::: xs))
SThere :: forall x y xs (e :: Elem x xs). SElem e -> SElem ('There e :: Elem x (y '::: xs))
type family RemoveElem (xs :: Vect (S n) a) (e :: Elem x xs) :: Vect n a
注意removeElem
和RemoveElem
类型之间的关系。参数的重新排序是因为 e
的类型取决于 xs
,因此需要相应地对它们进行排序。或者:xs
参数从 forall
'd-and-implicitly-given 提升为 explicitly-given,然后 Sing xs
参数被否决,因为它不包含任何信息,由于单身人士。
终于可以写这个函数了:
sRemoveElem :: forall (xs :: Vect (S n) Nat) (e :: Elem x xs).
SElem e -> SNatVect xs -> SNatVect (RemoveElem xs e)