标签: agda

Agda是一种很好的编程语言,可以探索依赖类型并使用直觉类型理论并尝试实现这些东西.但是,已经有用Agda编写的"真实"程序的例子吗？也许甚至可以展示其功能的例子(类似于xmonad经常被提到作为"真正的"Haskell程序的一个例子)？

在Agda邮件列表中,Conor McBride问道:

有没有办法像假定的那样掌握行动

   trustFromJust :: Maybe x -> x

Run Code Online (Sandbox Code Playgroud)

如果没有任何东西,它实际上并没有检查Just and Goes Wrong(在Milner的意义上)？

Agda可能会证明Maybe a == Just1 a,并且可以消除sum类型的中间构造函数.

我可以想到使用unsafeCoerce#或unpackClosure#的方法,但其他人是否有想法？

import GHC.Prim

trustFromJust :: Maybe x -> x
trustFromJust x = y
    where Just1 y = unsafeCoerce# x

data Just1 a = Just1 a

虽然这个段错误(单个构造函数类型可以避免一些闭包开销).核心看起来不错:

main2 =
  case (Data.Maybe.Just @ Type.Integer main3)
       `cast`
       (CoUnsafe
         (Data.Maybe.Maybe Type.Integer)
         (Just1 Type.Integer)
               :: Data.Maybe.Maybe Type.Integer
                    ~
                  Just1 Type.Integer)
  of _ { Just1 y_aeb ->
  $wshowsPrec 0 y_aeb ([] @ Char)

我注意到自从HoTT以来,"Axiom K"的讨论经常出现.我相信它与模式匹配有关.我很惊讶我在TAPL,ATTAPL或PFPL中找不到参考.

• 什么是Axiom K？
• 它是否用于ML样式的模式匹配,如SML(或只是依赖模式匹配)？
• 什么是Axiom K的适当参考？

我正在努力学习agda.但是,我遇到了问题.我在agda wiki上找到的所有教程对我来说都太复杂了,涵盖了编程的不同方面.在阅读了关于agda的3个教程之后,我能够编写简单的证明,但我仍然没有足够的知识将它用于真正的单词算法正确性.

你能推荐我关于这个主题的任何教程吗？类似于学习自己一个Haskell,但对于Agda.

我正在尝试根据我在Haskell中编写的程序将一些指称语义编码到Agda中.

data Value = FunVal (Value -> Value)
           | PriVal Int
           | ConVal Id [Value]
           | Error  String

在阿格达,直接翻译将是;

data Value : Set where
    FunVal : (Value -> Value) -> Value
    PriVal : ? -> Value
    ConVal : String -> List Value -> Value
    Error  : String -> Value

但是我得到了与FunVal有关的错误,因为;

值并非严格为正,因为它出现在Value定义中构造函数FunVal类型中箭头的左侧.

这是什么意思？我可以用Agda编码吗？我是以错误的方式去做的吗？

谢谢.

这种So类型的目的是什么？音译到Agda:

data So : Bool ? Set where
  oh : So true

So将布尔命题提升为逻辑命题.Oury和Swierstra的介绍性论文"Pi的力量"给出了一个由表格列索引的关系代数的例子.取两个表的产品要求它们具有不同的列,他们使用这些列So:

Schema = List (String × U)  -- U is the universe of SQL types

-- false iff the schemas share any column names
disjoint : Schema -> Schema -> Bool
disjoint = ...

data RA : Schema ? Set where
  -- ...
  Product : ? {s s'} ? {So (disjoint s s')} ? RA s ? RA s' ? RA …

我想有一个归纳类型来描述排列及其对某些容器的行为.很明显,根据这种类型的描述,算法的定义复杂度(就其长度而言)(计算组合或逆,分解成不相交的循环等)将会变化.

考虑Coq中的以下定义.我认为这是Lehmer代码的形式化:

Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).

很容易在大小为n的向量上定义它的动作,在其他容器上稍微硬一些,并且(至少对我而言)很难找到组合的形式化或逆向.

或者,我们可以将置换表示为具有属性的有限映射.可以容易地定义组合或逆,但是将其分解成不相交的循环是困难的.

所以我的问题是:是否有任何文件可以解决这个权衡问题？我设法找到的所有工作都处理了命令式设置中的计算复杂性,而我对"推理复杂性"和函数式编程感兴趣.

是否有类型化的编程语言,我可以约束类型,如下面的两个例子？

1. 概率是一个浮点数,最小值为0.0,最大值为1.0.

   type Probability subtype of float
   where
       max_value = 0.0
       min_value = 1.0
   

   Run Code Online (Sandbox Code Playgroud)

2. 离散概率分布是一个映射,其中:键应该都是相同的类型,值都是概率,值的总和= 1.0.

   type DPD<K> subtype of map<K, Probability>
   where
       sum(values) = 1.0
   

   Run Code Online (Sandbox Code Playgroud)

据我所知,Haskell或Agda无法做到这一点.

我是依赖类型的新手,我对这两者之间的区别感到困惑.看来人们通常说一个类型是由其他类型的参数,并通过一定的价值索引.但是,依赖类型语言中的类型和术语之间没有区别吗？参数和指数之间的区别是否基本？你能告诉我在编程和定理证明中它们的含义不同的例子吗？

我在Coq的SSReflect扩展中找到了两个公约,这些公约看起来特别有用,但我还没有看到在新的依赖类型语言(Lean,Agda,Idris)中广泛采用的公约.

首先,可能的谓词表示为布尔返回函数,而不是归纳定义的数据类型.这默认带来可判定性,通过计算开辟了更多的证明机会,并通过避免校对引擎携带大量证明条件来提高检查性能.我看到的主要缺点是需要使用反射词来在证明时操纵这些布尔谓词.

其次,具有不变量的数据类型被定义为包含简单数据类型和不变量证明的从属记录.例如,固定长度序列在SSReflect中定义,如:

Structure tuple_of : Type := Tuple {tval :> seq T; _ : size tval == n}.

A seq和证明该序列的长度是一定值.这与Idris如何定义此类型相反:

data Vect : (len : Nat) -> (elem : Type) -> Type 

一种依赖类型的数据结构,其中不变量是其类型的一部分.SSReflect方法的一个优点是它允许重用,因此例如许多定义的函数seq和关于它们的证明仍然可以使用tuple(通过对底层操作seq),而使用Idris的方法函数reverse,append等等需要被重写Vect.Lean实际上在其标准库中具有等效的SSReflect样式vector,但它也具有Idris样式array,似乎在运行时具有优化的实现.

一本面向SSReflect的书甚至声称Vect n A风格方法是反模式:

依赖类型语言和Coq中的常见反模式特别是将这样的代数属性编码到数据类型和函数本身的定义中(这种方法的规范示例是长度索引列表).虽然这种方法看起来很吸引人,因为它展示了依赖类型捕获它们的数据类型和函数的某些属性的能力,但它本质上是不可扩展的,因为总会有另一个感兴趣的属性,这是设计者没有预见到的.数据类型/函数的数据,因此它必须被编码为外部事实.这就是为什么我们提倡这种方法,其中数据类型和函数被定义为尽可能接近程序员定义的方式,并且它们的所有必要属性都是分开证明的.

因此,我的问题是,为什么没有更广泛地采用这些方法.我缺少哪些缺点,或者它们的优势在具有比Coq更好支持依赖模式匹配的语言中不那么重要？