小编Mus*_*ssy的帖子

Monads可以被解释为容器的形式:

• list:给定类型的项目的聚合
• bag:无序聚合
• set:忽略多重性的无序聚合
• 也许:最多一个项目的聚合
• 读者e:基数的汇总| e |

我想知道如何在这个视图中以一种有意义的方式将continuation解释为包/容器的形式.谢谢!

Agda的记录和instance关键字的混合使我们的行为类似于Haskell的类型类.而且,忽略instance关键字,我们可以为同一类型设置多个实例 - 这是我们在Haskell中无法做到的.

我正处于需要Haskell的单实例要求的地步,但在Agda中.是否有编译器选项或一些技巧/启发式来强制执行此操作？

现在我采取的方法是,

record Yo (n : ?) : Set where
  field
    sem : (some interesting property involving n)

open Yo {{...}}

postulate UniqueYo: ? {n} (p q : Yo n) ? p ? q

然而,每当我实际使用UniqueYo缺乏计算时,我的目标就会充斥着...| UniqueYo p p我喜欢的地方...| refl或完全重写为正常形式的东西.

任何帮助表示赞赏!

我希望能够在C#中创建一个方法,其输出类型取决于它的参数值; 松散,

delegate B(a) DFunc<A,B>(A a);

作为一个例子,我想编写一个函数,它接受一个整数并根据参数返回许多可能类型中的一个:

f(1) = int
f(2) = bool
f(3) = string
f(n), where n >= 4 = type of n-by-n matrices

任何帮助都会有用.

我想知道Agda中是否有类似于Haskell deriving Eq条款的内容 - 那么我下面也有一个相关的问题.

例如,假设我有玩具语言的类型,

data Type : Set where
  Nat  : Type
  Prp : Type

然后我可以通过模式匹配实现可判定的相等性C-c C-a,

_??_ : Decidable {A = Type} _?_
Nat ?? Nat = yes refl
Nat ?? Prp = no (? ())
Prp ?? Nat = no (? ())
Prp ?? Prp = yes refl

我很好奇这是否可以机械化或自动化,以某种方式类似于在Haskell中完成的方式:

data Type = Nat | Prp deriving Eq

谢谢!

虽然我们讨论类型的主题,但我想将我的正式类型视为Agda类型:Nat只是自然数,而Prp是小命题.

?_?Type : Type ? Set ?
? Nat ?Type = ?
? Prp ?Type …

我想使用除了作为类型构造函数给出的语法之外声明的语法自动判断参数.例如,

postulate P : ? ? ? ? Set

data Silly : Set where
  goo : (n : ?) ? Fin n ? (m : ?) ? Fin m ? P n m ? Silly

在这里,我想P n m在n和m参数之间进行证明,但这不可能是因为两者都需要声明才能表达.因此,我们使用语法声明:

syntax goo n i m j pf = i ?[ n , pf , m ]? j

现在,我们可以手工编写

want-to-use-syntax-in-pattern-matching : Silly ? Set
want-to-use-syntax-in-pattern-matching (i ?[ n , pf , m ]? j) = ?

这工作正常,但是当我通过case分割时 …

我正在使用lhs2TeX作为我的文字Agda文件,我希望它们能够突出显示语法.我知道我可以通过%format指令实现一些突出显示,但这有点太多了.我已按照http://foswiki.cs.uu.nl/foswiki/pub/FPOld/CourseLiterature/presentation.pdf的说明尝试使用lhs2Tex-hl,但无济于事.

如果有人可以帮助用彩色Agda获取PDF,那将不胜感激!

编辑

Agda乳胶后端很棒但有一些问题.最大的问题是spec-environment.它说规范是未定义的,所以把它作为一个同义词code应该修复:\newenvironment{spec}{\begin{code}}{\end{code}}但现在有类型检查问题和missing $错误.使用sed删除spec块会导致missing $错误; 同样\newenvironment{spec}{\verbatim}{\endverbatim}.使用时遇到类似问题|...|.另外,我真的很喜欢%formatlhs2tex ......

似乎为了证明记录类型的两个项目是等效的，我需要编写一个助手来获取组件明智的证明并应用它们。\n示例：

postulate P : \xe2\x84\x95 \xe2\x86\x92 Set\n\nrecord Silly : Set (\xe2\x84\x93suc \xe2\x84\x93\xe2\x82\x80) where\n constructor _#_#_\n field\n  n : \xe2\x84\x95\n  pn : P n\n  f : Set \xe2\x86\x92 \xe2\x84\x95\n\nopen Silly\n\nSillyEq : \xe2\x88\x80 s t \xe2\x86\x92 n s \xe2\x89\xa1 n t \xe2\x86\x92 pn s \xe2\x89\x85 pn t \xe2\x86\x92 f s \xe2\x89\xa1 f t \xe2\x86\x92 s \xe2\x89\xa1 t\nSillyEq (n # pn # f) (.n # .pn # .f) \xe2\x89\xa1-refl \xe2\x89\x85-refl \xe2\x89\xa1-refl = \xe2\x89\xa1-refl\n

我感到SillyEq应该以某种方式提供给我，我不需要自己写它——或者我错了。

另外，我无法证明SillyEq另外，如果不声明构造函数然后对其进行模式匹配，

在Haskell中,我们可以对二进制操作?进行分区以获得两个函数 (x ?)和(? y).据我所知,我们可以通过写作来模仿第一部分,_?_ x但我们可以干净利落地完成第二部分吗？

示例 这里我定义了已经分段的Agda库版本,Function._$_以执行上面提到的第二部分.但是,它在下面我想要的情况下不起作用,我不知道为什么.欢迎任何见解!

$ : ? {a b} {A : Set a} {B : A ? Set b} ? (x : A) ? ((y : A) ? B y) ? B x
$ x = ? f ? f x

success-usage : ?{a b}{A : Set a}{B : Set b} ? A ? (A ? B) ? B
success-usage x = $ x

failed-usage : ?{A : …

使用子集的概念作为谓词,

? : ? {b a} ? Set a ? Set (a ? suc b)
? {b} {a} X = X ? Set b

我想考虑赋予子集谓词的结构,

record SetWithAPredicate {a c} : Set {!!} where
  field
   S : Set a
   P : ? {b} ? ? {b} S ? Set c

由于使用了水平量化,这是一个结构不良的结构?.当我S, P用作模块的参数时,一切正常,但我希望它们是记录,以便我可以在它们上形成构造并给出它们的实例.

我尝试了一些其他的东西,比如通过存在主义来移动定义内部的水平b,?但这导致了可能性的麻烦.我也尝试过更改类型P,

P : ? {a} S ? Set c

但是我再也不能要求空集来拥有这个属性了:

P-? : P(? _ ? ?)

这是打字不好,因为Set != …

假设我有一个传递关系~有两个endomaps f和g.假设f并且g在任何地方f a ~ f b ~ f c 都同意然后有两种方式可以显示g a ~ g c:通过给定的等式将每个f转换为a g然后应用传递性,或者应用传递性然后沿着相等性转换.结果证明是否相同？显然是这样,

open import Relation.Binary.PropositionalEquality

postulate A : Set
postulate _~_  : A ? A ? Set
postulate _?~~?_ : ?{a b c} ? a ~ b ? b ~ c ? a ~ c
postulate f g : A ? A

subst-dist : ?{a b c}{ef : f a ~ f …