标签: idris

所以我最近一直在阅读有关coinduction的内容,现在我想知道:Haskell列出了归纳还是共同？我也听说Haskell没有区分这两者,但如果是这样的话,他们怎么这样做呢？

列表是归纳定义的data [a] = [] | a : [a],但可以共同使用,ones = a:ones.我们可以创建无限列表.然而,我们可以创建有限列表.他们是哪一个？

相关的是Idris,其中类型List a严格地是归纳类型,因此仅是有限列表.它的定义类似于Haskell中的方式.然而,Stream a是一种共同类型,建模无限列表.它被定义为(或者更确切地说,定义相当于)codata Stream a = a :: (Stream a).创建无限List或有限Stream是不可能的.但是,当我写出定义时

codata HList : Type -> Type where
    Nil : HList a
    Cons : a -> HList a -> HList a

我得到了我对Haskell列表的期望,即我可以创建有限和无限结构.

所以让我把它们归结为几个核心问题:

1. Haskell不区分归纳和共感类型吗？如果是这样,那是什么形式化？如果没有,那么哪个是[a]？

2. HList是coinductive吗？如果是这样,coinductive类型如何包含有限值？

3. 如果我们定义data HList' a = L (List a) | R (Stream a)怎么办？会考虑什么和/或仅对它有用HList？

在Haskell中,我可能会这样实现if:

if' True  x y = x
if' False x y = y
spin 0 = ()
spin n = spin (n - 1)

这表现我的期望:

haskell> if' True  (spin 1000000) ()  -- takes a moment
haskell> if' False (spin 1000000) ()  -- immediate

在Racket中,我可以实现这样的缺陷if:

(define (if2 cond x y) (if cond x y))
(define (spin n) (if (= n 0) (void) (spin (- n 1))))

这表现我的期望:

racket> (if2 …

所以在Idris中写下面的内容是完全有效的.

item : (b : Bool) -> if b then Nat else List Nat
item True  = 42
item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A

没有类型签名,这看起来像一个动态类型的语言.但实际上,伊德里斯是依赖性的.具体类型item b只能在运行期间确定.

当然,这是一个Haskell程序员所说的:item bIdris意义上的类型是在编译时给出的,它是if b then Nat ....

现在我的问题:我是否正确地得出结论,在Haskell中,运行时和编译时之间的边界恰好在值的世界(False,"foo",3)和类型的世界(Bool,String,Integer)之间运行,而在Idris中,运行时和编译时之间的边界跨越了宇宙？

另外,我是否正确地假设即使在Haskell中使用依赖类型(使用DataKinds和TypeFamilies,参见本文),上面的例子在Haskell中是不可能的,因为与Idris相反的Haskell不允许值泄漏到类型级别？

这种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 …

我目前正在使用Idris书籍进行类型驱动开发.

我在第6章中有两个与示例数据存储设计有关的问题.数据存储是一个命令行应用程序,允许用户设置存储在其中的数据类型,然后添加新数据.

以下是代码的相关部分(略有简化).你可以在Github上看到完整的代码:

module Main

import Data.Vect

infixr 4 .+.

-- This datatype is to define what sorts of data can be contained in the data store.
data Schema
  = SString
  | SInt
  | (.+.) Schema Schema

-- This is a type-level function that translates a Schema to an actual type.
SchemaType : Schema -> Type
SchemaType SString = String
SchemaType SInt = Int
SchemaType (x .+. y) = (SchemaType x, SchemaType y)

-- …

我所说的是无法定义:

data A = A {name :: String}
data B = B {name :: String}

我知道GHC只是将其解释为普通函数,解决这个问题的惯用方法是:

data A = A {aName :: String}
data B = B {bName :: String}

class Name a where
  name :: a -> String

instance Name A where
  name = aName

instance Name B where
  name = bName

写完这篇文章之后,我不太喜欢它......难道这个类型化不能成为荒谬过程的一部分吗？

当我写一些Aeson JSON解析时,我想到了这个想法.如果只是为每种数据类型派生FromJSON实例都太容易了,我必须手工编写所有内容(目前> 1k行和计数).拥有像name或简单地value在数据记录中的名称并不常见.

http://www.haskell.org/haskellwiki/Performance/Overloading提到函数重载会引入一些运行时开销.但实际上我不明白为什么编译器无法在编译时解析它并在内部给它们不同的名称.

这个来自2012年的SO问题或多或少地说明了历史原因并指出了2006年的邮件主题.最近有什么变化吗？

即使存在一些运行时开销,大多数人也不会介意,因为大多数代码几乎不是性能关键.

是否有一些隐藏的语言扩展实际允许这个？我不确定......但我认为伊德里斯实际上是这样做的？

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

我在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更好支持依赖模式匹配的语言中不那么重要？

在Idris 效果库中,效果表示为

||| This type is parameterised by:
||| + The return type of the computation.
||| + The input resource.
||| + The computation to run on the resource given the return value.
Effect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type

如果我们允许资源成为值并交换前两个参数,我们得到(其余代码在Agda中)

Effect : Set -> Set
Effect R = R -> (A : Set) -> (A -> R) -> Set

拥有一些基本的类型 - 上下文 - 会员机制

data Type : Set …

Idris在矢量引擎下做了什么样的优化吗？因为从它的外观来看,Idris向量只是一个已知大小的链表(在编译时已知).事实上,一般来说,你似乎可以表达以下等价(我在语法上有点猜测):

Vector : Nat -> Type -> Type
Vector n t = (l: List t ** length l = n)

因此,虽然这在防止范围误差方面很好,但是矢量的真正优势(在该术语的传统用法中)是在性能方面; 特别是O(1)随机访问.似乎idris向量不支持这个(你如何编写索引函数来获得这种性能？).

• 假设Nat在重新配置Vectors 之下没有任何巫术(如果发生的那样),Idris中是否存在随机访问数据类型？
• 如何在代数类型系统中定义这样的东西？当然,似乎不可能以归纳的方式定义它.
• 在像Idris这样的类型系统中,是否有可能创建一个支持O(1)随机访问的数据类型,并且知道它的长度使得所有访问都可证明是有效的？(Haskell有数组样式的向量,但它们的具体实现对普通用户来说是不透明的,包括我)