3

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函数，布尔值和参数类型之间应该存在一对一的对应关系（如果我传递一些其他类型，则不能进行类型检查）。

当然，我理解，这在一般情况下是不可能的。此类编译器技巧要求我的函数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

但我不明白如何在我的例子中使用这样的证明。如果这是不可能的，那么编写此类函数的最佳方法是什么？

4

1 回答 1

6

关键字基本上告诉 Idris，“为我找到这种类型的auto任何值”。因此，除非该类型仅包含一个值，否则您可能会得到错误的答案。伊德里斯看到{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当类型远大于两个或尝试推断多个值时，不能很好地扩展。

将上面示例中信息流的从左到右的性质与常规非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])

预测机器何时能或不能猜出你的意思是依赖类型编程的一项重要技能；您会发现自己在获得更多经验后会变得更好。

当然，在这种情况下，这一切都没有实际意义，因为列表已经具有一个或多个语义。将你的函数写在普通的旧列表上；然后，如果您需要将其应用于单个值，则可以将其包装在单例列表中。

于 2016-12-26T14:39:00.927 回答