如何让 ghc 相信类型级别的加法是可交换的(以实现依赖类型的反向)?
How to convince ghc that type level addition is commutative (to implement dependently typed reverse)?
这不会编译,因为 ghc 告诉我 Add 不是单射的。我如何告诉编译器 Add 确实是可交换的(也许通过告诉它 Add 是单射的)?从hasochism paper看来,必须以某种方式提供代理。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
data Nat = Z | S Nat
type family Add a b where
Add Z n = n
Add n Z = n
Add (S n) k = S (Add n k)
data VecList n a where
Nil :: VecList Z a
Cons :: a -> VecList n a -> VecList (S n) a
safeRev :: forall a n . VecList n a -> VecList n a
safeRev xs = safeRevAux Nil xs
where
safeRevAux :: VecList p a -> VecList q a -> VecList (Add p q) a
safeRevAux acc Nil = acc
safeRevAux acc (Cons y ys) = safeRevAux (Cons y acc) ys
一个人可以做到这一点,但我觉得幕后发生的事情太多了。
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Proxy
import Data.Type.Equality
data Nat = Z | S Nat
type family n1 + n2 where
Z + n2 = n2
(S n1) + n2 = S (n1 + n2)
-- singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
-- inductive proof of right-identity of +
plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
-- inductive proof of simplification on the rhs of +
plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
plus_succ_r SZero _ = Refl
plus_succ_r (SSucc n1) proxy_n2 = gcastWith (plus_succ_r n1 proxy_n2) Refl
data VecList n a where
V0 :: VecList Z a
Cons :: a -> VecList n a -> VecList (S n) a
reverseList :: VecList n a -> VecList n a
reverseList V0 = V0
reverseList list = go SZero V0 list
where
go :: SNat n1 -> VecList n1 a-> VecList n2 a -> VecList (n1 + n2) a
go snat acc V0 = gcastWith (plus_id_r snat) acc
go snat acc (Cons h (t :: VecList n3 a)) =
gcastWith (plus_succ_r snat (Proxy :: Proxy n3))
(go (SSucc snat) (Cons h acc) t)
safeHead :: VecList (S n) a -> a
safeHead (Cons x _) = x
test = safeHead $ reverseList (Cons 'a' (Cons 'b' V0))
请参阅 https://www.haskell.org/pipermail/haskell-cafe/2014-September/115919.html 了解原始想法。
编辑:
@user3237465 这很有趣,更符合我的想法
(虽然经过反思我的问题可能不是很好
制定)。
我好像有"axioms"
type family n1 :+ n2 where
Z :+ n2 = n2
(S n1) :+ n2 = S (n1 + n2)
因此可以产生像
这样的证明
plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
我觉得这很简洁。我通常会这样推理
- 在上面的最后一个子句中我们有 SSucc n :: SNat (S k) 所以 n :: k
- 因此我们需要证明 S k + Z :~: S k
- 由第二个"axiom" S k + Z = S (k + Z)
- 因此我们需要证明 S (k + Z) :~: S k
- plus_id_r n 给出一个 "proof" 即 (k + Z) :~: k
- 并且 Refl 给出了 "proof" m ~ n => S m :~: S n
- 因此,我们可以使用 gcastWith 统一这些证明以给出所需的
结果。
对于你的解决方案,你给出 "axioms"
type family n :+ m where
Z :+ m = m
S n :+ m = n :+ S m
有了这些,(n + Z) :~: n 的证明将不起作用。
- 在最后一个子句中,SSucc x 的类型再次为 SNat (S k)
- 因此我们需要证明 S k :+ Z :~: S k
- 到第二个新的 "axiom" 我们有 S k + Z = k + S Z
- 因此我们需要证明 k + S Z :~: S k
- 所以我们有更复杂的东西要证明:-(
我可以从新的 "axiom" 产生原始秒的证明
second "axiom"(所以我的 second "axiom" 现在是引理?)。
succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl
所以现在我应该能够让原始校样发挥作用,但我
不确定目前如何。
到目前为止我的推理是否正确?
PS: ghc 同意我关于为什么正确身份存在的证明不起作用的推理
Could not deduce ((n1 :+ 'S 'Z) ~ 'S n1)
...
or from ((n1 :+ 'Z) ~ n1)
你可以稍微简化一下reverse
的定义:
{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
data Nat = Z | S Nat
data Vec a n where
Nil :: Vec a Z
(:::) :: a -> Vec a n -> Vec a (S n)
type family n :+ m where
Z :+ m = m
S n :+ m = n :+ S m
elim0 :: Vec a (n :+ Z) -> Vec a n
elim0 = undefined
accrev :: Vec a n -> Vec a n
accrev = elim0 . go Nil where
go :: Vec a m -> Vec a n -> Vec a (n :+ m)
go acc Nil = acc
go acc (x ::: xs) = go (x ::: acc) xs
(:+)
运算符是根据 (:::)
运算符定义的。 (:::)
案例中的统一过程如下:
x ::: xs
导致 n
成为 S n
。所以结果的类型变成 Vec a (S n :+ m)
或者,在 beta-reduction 之后,变成 Vec a (n :+ S m)
。而
x ::: acc :: Vec a (S m)
xs :: Vec a n
go (x ::: acc) xs :: Vec a (n :+ S m)
所以我们有一场比赛。但是现在您需要定义 elim0 :: Vec a (n :+ Z) -> Vec a n
,这需要您的问题的两个证明。
Agda 中的全部代码:http://lpaste.net/117679
顺便说一句,这不是真的,无论如何你都需要证据。以下是 reverse
在 Agda 标准库中的定义:
foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
(∀ {n} → B n → A → B (suc n)) →
B zero →
Vec A m → B m
foldl b _⊕_ n [] = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs
reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
那是因为 foldl
携带了关于 _⊕_
行为的额外类型信息,所以你在每一步都满足类型检查器的要求,不需要证明。
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitForAll #-}
import Data.Type.Equality
data Nat = Z | S Nat
type family (n :: Nat) :+ (m :: Nat) :: Nat where
Z :+ m = m
S n :+ m = n :+ S m
-- Singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl
plus_id_r :: SNat n -> ((n :+ Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc x) = gcastWith (plus_id_r x) (succ_plus_id x SZero)
data Vec a n where
Nil :: Vec a Z
(:::) :: a -> Vec a n -> Vec a (S n)
size :: Vec a n -> SNat n
size Nil = SZero
size (_ ::: xs) = SSucc $ size xs
elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n)
elim0 n x = gcastWith (plus_id_r n) x
accrev :: Vec a n -> Vec a n
accrev x = elim0 (size x) $ go Nil x where
go :: Vec a m -> Vec a n -> Vec a (n :+ m)
go acc Nil = acc
go acc (x ::: xs) = go (x ::: acc) xs
safeHead :: Vec a (S n) -> a
safeHead (x ::: _) = x
这不会编译,因为 ghc 告诉我 Add 不是单射的。我如何告诉编译器 Add 确实是可交换的(也许通过告诉它 Add 是单射的)?从hasochism paper看来,必须以某种方式提供代理。
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
data Nat = Z | S Nat
type family Add a b where
Add Z n = n
Add n Z = n
Add (S n) k = S (Add n k)
data VecList n a where
Nil :: VecList Z a
Cons :: a -> VecList n a -> VecList (S n) a
safeRev :: forall a n . VecList n a -> VecList n a
safeRev xs = safeRevAux Nil xs
where
safeRevAux :: VecList p a -> VecList q a -> VecList (Add p q) a
safeRevAux acc Nil = acc
safeRevAux acc (Cons y ys) = safeRevAux (Cons y acc) ys
一个人可以做到这一点,但我觉得幕后发生的事情太多了。
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
import Data.Proxy
import Data.Type.Equality
data Nat = Z | S Nat
type family n1 + n2 where
Z + n2 = n2
(S n1) + n2 = S (n1 + n2)
-- singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
-- inductive proof of right-identity of +
plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
-- inductive proof of simplification on the rhs of +
plus_succ_r :: SNat n1 -> Proxy n2 -> ((n1 + (S n2)) :~: (S (n1 + n2)))
plus_succ_r SZero _ = Refl
plus_succ_r (SSucc n1) proxy_n2 = gcastWith (plus_succ_r n1 proxy_n2) Refl
data VecList n a where
V0 :: VecList Z a
Cons :: a -> VecList n a -> VecList (S n) a
reverseList :: VecList n a -> VecList n a
reverseList V0 = V0
reverseList list = go SZero V0 list
where
go :: SNat n1 -> VecList n1 a-> VecList n2 a -> VecList (n1 + n2) a
go snat acc V0 = gcastWith (plus_id_r snat) acc
go snat acc (Cons h (t :: VecList n3 a)) =
gcastWith (plus_succ_r snat (Proxy :: Proxy n3))
(go (SSucc snat) (Cons h acc) t)
safeHead :: VecList (S n) a -> a
safeHead (Cons x _) = x
test = safeHead $ reverseList (Cons 'a' (Cons 'b' V0))
请参阅 https://www.haskell.org/pipermail/haskell-cafe/2014-September/115919.html 了解原始想法。
编辑:
@user3237465 这很有趣,更符合我的想法 (虽然经过反思我的问题可能不是很好 制定)。
我好像有"axioms"
type family n1 :+ n2 where
Z :+ n2 = n2
(S n1) :+ n2 = S (n1 + n2)
因此可以产生像
这样的证明plus_id_r :: SNat n -> ((n + Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc n) = gcastWith (plus_id_r n) Refl
我觉得这很简洁。我通常会这样推理
- 在上面的最后一个子句中我们有 SSucc n :: SNat (S k) 所以 n :: k
- 因此我们需要证明 S k + Z :~: S k
- 由第二个"axiom" S k + Z = S (k + Z)
- 因此我们需要证明 S (k + Z) :~: S k
- plus_id_r n 给出一个 "proof" 即 (k + Z) :~: k
- 并且 Refl 给出了 "proof" m ~ n => S m :~: S n
- 因此,我们可以使用 gcastWith 统一这些证明以给出所需的 结果。
对于你的解决方案,你给出 "axioms"
type family n :+ m where
Z :+ m = m
S n :+ m = n :+ S m
有了这些,(n + Z) :~: n 的证明将不起作用。
- 在最后一个子句中,SSucc x 的类型再次为 SNat (S k)
- 因此我们需要证明 S k :+ Z :~: S k
- 到第二个新的 "axiom" 我们有 S k + Z = k + S Z
- 因此我们需要证明 k + S Z :~: S k
- 所以我们有更复杂的东西要证明:-(
我可以从新的 "axiom" 产生原始秒的证明 second "axiom"(所以我的 second "axiom" 现在是引理?)。
succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl
所以现在我应该能够让原始校样发挥作用,但我 不确定目前如何。
到目前为止我的推理是否正确?
PS: ghc 同意我关于为什么正确身份存在的证明不起作用的推理
Could not deduce ((n1 :+ 'S 'Z) ~ 'S n1)
...
or from ((n1 :+ 'Z) ~ n1)
你可以稍微简化一下reverse
的定义:
{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
{-# LANGUAGE TypeFamilies, UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
data Nat = Z | S Nat
data Vec a n where
Nil :: Vec a Z
(:::) :: a -> Vec a n -> Vec a (S n)
type family n :+ m where
Z :+ m = m
S n :+ m = n :+ S m
elim0 :: Vec a (n :+ Z) -> Vec a n
elim0 = undefined
accrev :: Vec a n -> Vec a n
accrev = elim0 . go Nil where
go :: Vec a m -> Vec a n -> Vec a (n :+ m)
go acc Nil = acc
go acc (x ::: xs) = go (x ::: acc) xs
(:+)
运算符是根据 (:::)
运算符定义的。 (:::)
案例中的统一过程如下:
x ::: xs
导致 n
成为 S n
。所以结果的类型变成 Vec a (S n :+ m)
或者,在 beta-reduction 之后,变成 Vec a (n :+ S m)
。而
x ::: acc :: Vec a (S m)
xs :: Vec a n
go (x ::: acc) xs :: Vec a (n :+ S m)
所以我们有一场比赛。但是现在您需要定义 elim0 :: Vec a (n :+ Z) -> Vec a n
,这需要您的问题的两个证明。
Agda 中的全部代码:http://lpaste.net/117679
顺便说一句,这不是真的,无论如何你都需要证据。以下是 reverse
在 Agda 标准库中的定义:
foldl : ∀ {a b} {A : Set a} (B : ℕ → Set b) {m} →
(∀ {n} → B n → A → B (suc n)) →
B zero →
Vec A m → B m
foldl b _⊕_ n [] = n
foldl b _⊕_ n (x ∷ xs) = foldl (λ n → b (suc n)) _⊕_ (n ⊕ x) xs
reverse : ∀ {a n} {A : Set a} → Vec A n → Vec A n
reverse {A = A} = foldl (Vec A) (λ rev x → x ∷ rev) []
那是因为 foldl
携带了关于 _⊕_
行为的额外类型信息,所以你在每一步都满足类型检查器的要求,不需要证明。
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExplicitForAll #-}
import Data.Type.Equality
data Nat = Z | S Nat
type family (n :: Nat) :+ (m :: Nat) :: Nat where
Z :+ m = m
S n :+ m = n :+ S m
-- Singleton for Nat
data SNat :: Nat -> * where
SZero :: SNat Z
SSucc :: SNat n -> SNat (S n)
succ_plus_id :: SNat n1 -> SNat n2 -> (((S n1) :+ n2) :~: (S (n1 :+ n2)))
succ_plus_id SZero _ = Refl
succ_plus_id (SSucc n) m = gcastWith (succ_plus_id n (SSucc m)) Refl
plus_id_r :: SNat n -> ((n :+ Z) :~: n)
plus_id_r SZero = Refl
plus_id_r (SSucc x) = gcastWith (plus_id_r x) (succ_plus_id x SZero)
data Vec a n where
Nil :: Vec a Z
(:::) :: a -> Vec a n -> Vec a (S n)
size :: Vec a n -> SNat n
size Nil = SZero
size (_ ::: xs) = SSucc $ size xs
elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n)
elim0 n x = gcastWith (plus_id_r n) x
accrev :: Vec a n -> Vec a n
accrev x = elim0 (size x) $ go Nil x where
go :: Vec a m -> Vec a n -> Vec a (n :+ m)
go acc Nil = acc
go acc (x ::: xs) = go (x ::: acc) xs
safeHead :: Vec a (S n) -> a
safeHead (x ::: _) = x