不规则孔型分辨率

我最近发现，在哈斯克尔，打字孔与校样上的模式匹配结合在一起，提供了一种非常不错的类似《阿格达》(agda)的体验。例如:

{-# LANGUAGE
DataKinds, PolyKinds, TypeFamilies,
UndecidableInstances, GADTs, TypeOperators #-}


data (==) :: k -> k -> * where
Refl :: x == x


sym :: a == b -> b == a
sym Refl = Refl


data Nat = Zero | Succ Nat


data SNat :: Nat -> * where
SZero :: SNat Zero
SSucc :: SNat n -> SNat (Succ n)


type family a + b where
Zero   + b = b
Succ a + b = Succ (a + b)


addAssoc :: SNat a -> SNat b -> SNat c -> (a + (b + c)) == ((a + b) + c)
addAssoc SZero b c = Refl
addAssoc (SSucc a) b c = case addAssoc a b c of Refl -> Refl


addComm :: SNat a -> SNat b -> (a + b) == (b + a)
addComm SZero SZero = Refl
addComm (SSucc a) SZero = case addComm a SZero of Refl -> Refl
addComm SZero (SSucc b) = case addComm SZero b of Refl -> Refl
addComm sa@(SSucc a) sb@(SSucc b) =
case addComm a sb of
Refl -> case addComm b sa of
Refl -> case addComm a b of
Refl -> Refl

真正好的事情是，我可以用一个类型孔来替换 abc0结构的右侧，我的 hole 目标类型用证明进行了更新，就像 Agda 的 abc1表单一样。

然而，有时候这个漏洞就是无法更新:

(+.) :: SNat a -> SNat b -> SNat (a + b)
SZero   +. b = b
SSucc a +. b = SSucc (a +. b)
infixl 5 +.


type family a * b where
Zero   * b = Zero
Succ a * b = b + (a * b)


(*.) :: SNat a -> SNat b -> SNat (a * b)
SZero   *. b = SZero
SSucc a *. b = b +. (a *. b)
infixl 6 *.


mulDistL :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL SZero b c = Refl
mulDistL (SSucc a) b c =
case sym $ addAssoc b (a *. b) (c +. a *. c) of
-- At this point the target type is
-- ((b + c) + (n * (b + c))) == (b + ((n * b) + (c + (n * c))))
-- The next step would be to update the RHS of the equivalence:
Refl -> case addAssoc (a *. b) c (a *. c) of
Refl -> _ -- but the type of this hole remains unchanged...

此外，即使目标类型不一定在证明内部排成一行，如果我粘贴来自 Agda 的整个过程，它仍然可以检查:

mulDistL' :: SNat a -> SNat b -> SNat c -> (a * (b + c)) == ((a * b) + (a * c))
mulDistL' SZero b c = Refl
mulDistL' (SSucc a) b c = case
(sym $ addAssoc b (a *. b) (c +. a *. c),
addAssoc (a *. b) c (a *. c),
addComm (a *. b) c,
sym $ addAssoc c (a *. b) (a *. c),
addAssoc b c (a *. b +. a *. c),
mulDistL' a b c
) of (Refl, Refl, Refl, Refl, Refl, Refl) -> Refl

你知道为什么会发生这种情况吗(或者我如何能够以一种健壮的方式进行证明重写) ？

2280 次浏览
小开

It happens because the values are determined at run time. It can bring about a transformation of values depending on what are entered at run time hence it assumes that the hole is already updated.

小开

If you want to generate all possible such values, then you can write a function to do so, either with provided or specified bounds.

It may very well be possible to use type-level Church Numerals or some such so as to enforce creation of these, but it's almost definitely too much work for what you probably want/need.

This might not be what you want (i.e. "Except of using just (x, y) since z = 5 - x - y") but it makes more sense than trying to have some kind of enforced restriction on the type level for allowing valid values.


提交答案