在Agda中使用字符串作为键进行映射? [英] Map with Strings as Keys in Agda?
问题描述
我在弄清楚如何正确地在Agda中使用String键制作Map时遇到了一些麻烦.我有以下内容:
I'm having some trouble figuring out how to properly make a Map with String keys in Agda. I've got the following:
import Data.AVL.IndexedMap
Var = String
data Type where -- ...
alwaysType : Var -> Set
alwaysType _ = Type
open Data.AVL.IndexedMap alwaysType (StrictTotalOrder.isStrictTotalOrder Data.String.strictTotalOrder)
这给出了错误:
String != Σ String _Key_90 of type Set
when checking that the expression
StrictTotalOrder.isStrictTotalOrder strictTotalOrder has type
Relation.Binary.IsStrictTotalOrder .Agda.Builtin.Equality._≡_
__<__91
打开地图"模块的正确方法是什么?
What is the proper way to open the Map module?
推荐答案
Data.AVL.IndexedMap
模块用于(有限)映射,其中存在键和值的类型族,以及与给定键关联的值与值共享索引.
The Data.AVL.IndexedMap
module is for (finite) maps where there is a family of types for the keys and the values, and the value associated with a given key shares the index with the value.
这不是您想要的,因为您希望所有键都为String
s.因此,只需使用Data.AVL
(即具有未索引键的版本):
This is not what you want here, since you want all your keys to be String
s. So just use Data.AVL
(i.e. the version with non-indexed keys):
open import Data.String using (String)
open import Function using (const)
Key = String
postulate
Value : Set
open import Relation.Binary using (StrictTotalOrder)
open import Data.AVL (const Value) (StrictTotalOrder.isStrictTotalOrder Data.String.strictTotalOrder)
不幸的是,这仍然没有进行类型检查:
Unfortunately, this still doesn't typecheck:
.Relation.Binary.List.Pointwise.Rel
(StrictTotalOrder._≈_ .Data.Char.strictTotalOrder)
(Data.String.toList x) (Data.String.toList x₁)
!= x .Agda.Builtin.Equality.≡ x₁ of type Set
when checking that the expression
StrictTotalOrder.isStrictTotalOrder Data.String.strictTotalOrder
has type IsStrictTotalOrder .Agda.Builtin.Equality._≡_ __<__10
这是因为Data.String.strictTotalOrder
使用逐点相等(在组成String
的Char
的Char
的ℕ
值的列表上),并且Data.AVL
需要命题相等.因此,完全相同的示例将适用于例如ℕ
键:
That's because Data.String.strictTotalOrder
uses pointwise equality (over the list of ℕ
values of the Char
s that make up the String
), and Data.AVL
requires propositional equality. So the exact same example would work with, e.g., ℕ
keys:
open import Data.Nat using (ℕ)
open import Function using (const)
Key = ℕ
postulate
Value : Set
import Data.Nat.Properties
open import Relation.Binary using (StrictTotalOrder)
open import Data.AVL (const Value) (StrictTotalOrder.isStrictTotalOrder Data.Nat.Properties.strictTotalOrder)
因此下一步需要将StrictTotalOrder.isStrictTotalOrder Data.String.strictTotalOrder
转换为IsStrictTotalOrder (_≡_ {A = String}) _
类型的东西.我现在暂时将其留给其他人,但是如果有时间,如果您无法正常工作并且也没有其他人来找它,我很乐意稍后再进行研究.
So the next step needs to be to transform StrictTotalOrder.isStrictTotalOrder Data.String.strictTotalOrder
into something of type IsStrictTotalOrder (_≡_ {A = String}) _
. I'll leave that to someone else for now, but I'm happy to look into it later, when I have the time, if you can't get it working and noone else picks it up either.
编辑后添加:这是一种(可能非常复杂)将标准库中的StrictTotalOrder
String
转换为使用命题相等的方法:
EDITED TO ADD: Here's a (possibly horribly over-complicated) way of turning that StrictTotalOrder
for String
s from the standard lib into something that uses propositional equality:
open import Function using (const; _∘_; _on_)
open import Relation.Binary
open import Data.String
using (String; toList∘fromList; fromList∘toList)
renaming (toList to stringToList; fromList to stringFromList)
open import Relation.Binary.List.Pointwise as Pointwise
open import Relation.Binary.PropositionalEquality as P hiding (trans)
open import Data.Char.Base renaming (toNat to charToNat)
STO : StrictTotalOrder _ _ _
STO = record
{ Carrier = String
; _≈_ = _≡_
; _<_ = _<_
; isStrictTotalOrder = record
{ isEquivalence = P.isEquivalence
; trans = λ {x} {y} {z} → trans {x} {y} {z}
; compare = compare
}
}
where
open StrictTotalOrder Data.String.strictTotalOrder
renaming (isEquivalence to string-isEquivalence; compare to string-compare)
-- It feels like this should be defined somewhere in the
-- standard library, but I can't find it...
primCharToNat-inj : ∀ {x y} → primCharToNat x ≡ primCharToNat y → x ≡ y
primCharToNat-inj _ = trustMe
where
open import Relation.Binary.PropositionalEquality.TrustMe
open import Data.List
lem : ∀ {xs ys} → Pointwise.Rel (_≡_ on primCharToNat) xs ys → xs ≡ ys
lem [] = P.refl
lem {x ∷ xs} {y ∷ ys} (x∼y ∷ p) with primCharToNat-inj {x} {y} x∼y
lem {x ∷ xs} {_ ∷ ys} (x∼y ∷ p) | P.refl = cong _ (lem p)
≡-from-≈ : {s s′ : String} → s ≈ s′ → s ≡ s′
≡-from-≈ {s} {s′} p = begin
s ≡⟨ sym (fromList∘toList _) ⟩
stringFromList (stringToList s) ≡⟨ cong stringFromList (lem p) ⟩
stringFromList (stringToList s′) ≡⟨ fromList∘toList _ ⟩
s′ ∎
where
open P.≡-Reasoning
≈-from-≡ : {s s′ : String} → s ≡ s′ → s ≈ s′
≈-from-≡ {s} {_} refl = string-refl {s}
where
open IsEquivalence string-isEquivalence renaming (refl to string-refl) using ()
compare : (x y : String) → Tri (x < y) (x ≡ y) _
compare x y with string-compare x y
compare x y | tri< a ¬b ¬c = tri< a (¬b ∘ ≈-from-≡) ¬c
compare x y | tri≈ ¬a b ¬c = tri≈ ¬a (≡-from-≈ b) ¬c
compare x y | tri> ¬a ¬b c = tri> ¬a (¬b ∘ ≈-from-≡) c
这篇关于在Agda中使用字符串作为键进行映射?的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!