在Idris中自动检测依赖类型函数的域

Question

Idris语言教程有一个简单易懂的依赖类型概念示例:http: //docs.idris-lang.org/en/latest/tutorial/typesfuns.html#first-class-types

这是代码:

isSingleton : Bool -> Type
isSingleton True = Int
isSingleton False = List Int

mkSingle : (x : Bool) -> isSingleton x
mkSingle True = 0
mkSingle False = []

sum : (single : Bool) -> isSingleton single -> Int
sum True x = x
sum False [] = 0
sum False (x :: xs) = x + sum False xs

我决定花更多的时间在这个例子上.让我困扰的sum是我需要明确地将single : Bool值传递给函数.我不想这样做,我希望编译器猜测这个布尔值应该是什么.因此,我只传递Int或List Int向sum作用应该有布尔值和参数的类型之间1对1的对应关系(如果我通过一些其它类型的这只是不能键入检查).

当然,我理解,这在一般情况下是不可能的.这种编译器技巧要求我的函数isSingleton(或任何其他类似的函数)是单射的.但对于这种情况,它应该是可能的,因为在我看来......

所以我从下一个实现开始:我只是single隐含了参数.

sum : {single : Bool} -> isSingleton single -> Int
sum {single = True} x = x
sum {single = False} [] = 0
sum {single = False} (x :: xs) = x + sum' {single = False} xs

好吧,它并没有真正解决我的问题,因为我仍然需要以下一种方式调用此函数:

sum {single=True} 1

但我在教程中读到关于auto关键字的内容 虽然我不太明白是什么auto(因为我没有找到它的描述),我决定更多地补充我的功能:

sum' : {auto single : Bool} -> isSingleton single -> Int
sum' {single = True} x = x
sum' {single = False} [] = 0
sum' {single = False} (x :: xs) = x + sum' {single = False} xs

它适用于列表!

*DepFun> :t sum'
sum' : {auto single : Bool} -> isSingleton single -> Int
*DepFun> sum' [1,2,3]
6 : Int

但不适用于单一价值:(

*DepFun> sum' 3
When checking an application of function Main.sum':
        List Int is not a numeric type

有人可以解释一下,目前在这种内射函数用法中实际可能实现我的目标吗？我观看了这个关于证明某些事情的短视频是不完整的:https: //www.youtube.com/watch？v = 7Ml8u7DFgAk

但我不明白我的例子中如何使用这些证明.如果这不可能,那么编写这些函数的最佳方法是什么？

Answer 1

该auto关键字基本上告诉Idris,"找到我这种类型的任何价值".因此,除非该类型只包含一个值,否则您可能会得到错误的答案.伊德里斯看到{auto x : Bool}并填补了任何旧的Bool,即False.它不会使用其后来参数的知识来帮助它选择 - 信息不会从右向左流动.

一个解决方法是使信息在另一个方向上流动.而是使用上面的Universe样式构造,编写一个接受任意类型的函数,并使用谓词将其细化为您想要的两个选项.这样,Idris可以查看前面参数的类型,并选择IsListOrInt其类型匹配的唯一值.

data IsListOrInt a where
    IsInt : IsListOrInt Int
    IsList : IsListOrInt (List Int)

sum : a -> {auto isListOrInt : IsListOrInt a} -> Int
sum x {IsInt} = x
sum [] {IsList} = 0
sum (x :: xs) {IsList} = x + sum xs

现在,在这种情况下,搜索空间足够小(两个值 - True和False),Idris可以以蛮力的方式探索每个选项并选择第一个导致程序通过类型检查器,但该算法没有当类型大于2时,或者在尝试推断多个值时,不能很好地扩展.

将上例中信息流的从左到右的性质与常规非auto大括号的行为进行比较,这表明Idris 使用统一以双向方式查找结果.正如您所指出的,只有当所讨论的类型函数是单射函数时,才能成功.您可以将输入结构化为单独的索引数据类型,并允许Idris查看构造函数以b使用统一进行查找.

data OneOrMany isOne where
    One : Int -> OneOrMany True
    Many : List Int -> OneOrMany False

sum : {b : Bool} -> OneOrMany b -> Int
sum (One x) = x
sum (Many []) = 0
sum (Many (x :: xs)) = x + sum (Many xs)

test = sum (One 3) + sum (Many [29, 43])

预测机器何时或将无法猜出你的意思是依赖类型编程的一项重要技能; 你会发现自己越来越好,经验越来越好.

当然,在这种情况下,它完全没有用,因为列表已经有一个或多个语义.在普通的旧列表上写下你的功能; 然后,如果您需要将它应用于单个值,您可以将其包装在单个列表中.