不規則的孔類型分辨率

107

我最近發現，類型孔與證明上的模式匹配相結合，在Haskell中提供了非常好的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 [email protected](SSucc a) [email protected](SSucc b) = 
    case addComm a sb of 
     Refl -> case addComm b sa of 
      Refl -> case addComm a b of 
       Refl -> Refl

的真正好處是，我可以用一個類型孔替換Refl -> exp結構的右手邊，和我的洞目標類型與證據更新，幾乎與該rewrite形式在Agda。

但是，有時孔，只不過沒有更新：

(+.) :: 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...

而且，即使目標類型並不一定證明裏面排隊，如果我從阿格達整件事粘貼仍檢查罰款：

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

你有什麼想法解釋爲什麼會發生這種情況（或者我如何以強有力的方式進行證明重寫）？

來源

2014-02-27 András Kovács

你不期待多少？平等證明上的模式匹配是建立（雙向）平等。目前還不清楚您希望將其應用於目標類型的方向和方向。例如，你可以省略'mulDistL''中的'sym'調用，你的代碼仍然會檢查。 – kosmikus

很可能我期待太多。但是，在許多情況下，它的工作方式與Agda一樣，因此找出行爲的規律性仍然很有用。儘管如此，我並不樂觀，因爲這件事可能與類型檢查者的腸子有很深的關係。 –

這與你的問題有點正交，但你可以通過使用一組等同推理組合器àla Agda來證明這些證明。參看[這個概念驗證]（https://github.com/gallais/potpourri/blob/master/haskell/proofs/NatProofs.hs） – gallais