不规则的孔类型分辨率
我最近发现，类型孔与证明上的模式匹配相结合，在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 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
真正好的是，我可以用一个类型空洞替换Refl -> exp结构的右侧，并且我的空洞目标类型用证明进行更新，几乎与Agda中的rewrite表单一样。
但是，有时这个漏洞无法更新：
(+.) :: 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
你有什么想法，为什么会发生这种情况（或者我如何以强有力的方式进行证据重写）？
如果你想产生所有可能的这样的值，那么你可以编写一个函数来实现，可以使用提供的或指定的边界。
可能很有可能使用类型级别的教会数字或其他类型来强制创建这些数字，但对于您可能想要/需要的东西来说，它几乎肯定是太多的工作。
这可能不是你想要的（即“除了使用just（x，y），因为z = 5 - x - y”），但它比尝试对类型级别实施某种强制限制以允许有效更有意义值。
它发生是因为这些值是在运行时确定的。 它可以根据运行时输入的内容实现值的转换，因此它假定该孔已经更新。
链接地址: http://www.djcxy.com/p/43273.html