我正在Idris中编写一个基本的一元解析器,以习惯语法和与Haskell的差异。我有工作很好的基础知识,但我坚持尝试为解析器创建verifiedsemiggroup和VerifiedMonoid实例。
话不多说,下面是解析器类型、semiggroup和Monoid实例,以及verifiedsemiggroup实例的开始。
data ParserM a = Parser (String -> List (a, String))
parse : ParserM a -> String -> List (a, String)
parse (Parser p) = p
instance Semigroup (ParserM a) where
p <+> q = Parser (s => parse p s ++ parse q s)
instance Monoid (ParserM a) where
neutral = Parser (const [])
instance VerifiedSemigroup (ParserM a) where
semigroupOpIsAssociative (Parser p) (Parser q) (Parser r) = ?whatGoesHere
我基本上被困在intros
之后,具有以下证明者状态:
-Parser.whatGoesHere> intros
---------- Other goals: ----------
{hole3},{hole2},{hole1},{hole0}
---------- Assumptions: ----------
a : Type
p : String -> List (a, String)
q : String -> List (a, String)
r : String -> List (a, String)
---------- Goal: ----------
{hole4} : Parser (s => p s ++ q s ++ r s) =
Parser (s => (p s ++ q s) ++ r s)
-Parser.whatGoesHere>
看起来我应该能够在某种程度上使用rewrite
和appendAssociative
,但我不知道如何"进入"lambda s
。
无论如何,我被困在练习的定理证明部分-而且我似乎找不到太多以idris为中心的定理证明文档。我想也许我需要开始看Agda教程(尽管Idris是我确信我想学习的依赖类型语言!)。
简单的答案是你不能。在内涵类型理论中,关于函数的推理是相当尴尬的。例如,Martin-Löf的类型论无法证明:
S x + y = S (x + y)
0 + y = y
x +′ S y = S (x + y)
x +′ 0 = x
_+_ ≡ _+′_ -- ???
(据我所知,这是一个实际的定理,而不仅仅是"缺乏想象力的证明";然而,我找不到我阅读它的来源)。这也意味着没有证据证明更一般的:
ext : ∀ {A : Set} {B : A → Set}
{f g : (x : A) → B x} →
(∀ x → f x ≡ g x) → f ≡ g
这被称为函数可拓性:如果你能证明所有参数的结果是相等的(也就是说,函数在可拓性上是相等的),那么函数也相等。
这将完美地解决您的问题:
<+>-assoc : {A : Set} (p q r : ParserM A) →
(p <+> q) <+> r ≡ p <+> (q <+> r)
<+>-assoc (Parser p) (Parser q) (Parser r) =
cong Parser (ext λ s → ++-assoc (p s) (q s) (r s))
,其中++-assoc
是_++_
的结合律的证明。我不确定它在战术上会是什么样子,但它将是相当相似的:为Parser
应用一致性,目标应该是:
(s => p s ++ q s ++ r s) = (s => (p s ++ q s) ++ r s)
您可以应用可扩展性来获得假设s : String
和目标:
p s ++ q s ++ r s = (p s ++ q s) ++ r s
然而,正如我之前所说的,我们没有函数的延展性(注意,这对一般类型理论来说是不成立的:延展性类型理论,同伦类型理论和其他类型理论都能够证明这一点)。一个简单的选择是把它当作一个公理。与任何其他公理一样,您的风险是:
失去一致性(即能够证明错误;虽然我认为函数的可扩展性是OK的)
破缺约简(当给定此公理时,仅对
refl
进行案例分析的函数会做什么?)
我不确定Idris是如何处理公理的,所以我不会详细说明。只是要注意,如果你不小心的话,公理可能会把一些东西搞砸。
最难的选择是使用setoids。setoid基本上是一种配备了自定义相等的类型。这个想法是,而不是有一个Monoid
(或VerifiedSemigroup
在你的情况下),工作在内置的等式(=
在Idris, ≡
在Agda),你有一个特殊的monooid(或半群)与不同的底层相等。这通常是通过将单群(半群)操作与等式和一堆证明打包在一起来完成的,即(在伪代码中):
= : A → A → Set -- equality
_*_ : A → A → A -- associative binary operation
1 : A -- neutral element
=-refl : x = x
=-trans : x = y → y = z → x = z
=-sym : x = y → y = x
*-cong : x = y → u = v → x * u = y * v -- the operation respects
-- our equality
*-assoc : x * (y * z) = (x * y) * z
1-left : 1 * x = x
1-right : x * 1 = x
解析器的相等性选择是明确的:如果两个解析器的输出对所有可能的输入一致,则它们相等。
-- Parser equality
_≡p_ : {A : Set} (p q : ParserM A) → Set
Parser p ≡p Parser q = ∀ x → p x ≡ q x
这个解决方案有不同的权衡,即新的等式不能完全替代内置的等式(当您需要重写某些项时,往往会出现这种情况)。但如果你只是想显示你的代码做了它应该做的事情(直到一些自定义的相等),这是很好的。