自动检测IDRI中依赖类型功能的域

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功能，Boolean值和参数类型之间应该有1-1的对应关系（如果我通过其他类型，则不得键入检查）。

当然，我知道，这在通常的情况下是不可能的。这样的编译器技巧需要我的功能isSingleton（或任何其他类似功能）是 Injective 。但是对于这种情况，这应该是可能的，因为在我看来...

所以我从下一个实现开始：我刚刚使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，"找到我的任何值"。因此，除非该类型仅包含一个值，否则您有责任获得错误的答案。IDRIS看到{auto x : Bool}，并用任何旧的Bool填充它，即False。它没有使用以后的参数知识来帮助其选择 - 信息不会从右到左流。

一个修复程序是使信息流向另一个方向。宁愿使用上述宇宙式结构，而是编写一个接受任意类型的功能，并使用谓词将其完善为您想要的两个选项。这样，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可以以野蛮的方式探索所有选项，并选择第一个导致通过类型检查器的程序中的第一个选项，但是当类型大于两个时，或者在尝试推断多个值时，该算法并不能很好地扩展。

将上述示例中信息流的左右性质与常规非auto括号的行为进行比较，该括号指示IDRIS使用统一使用A bivecretional 时尚找到结果。如您所指出的那样，只有在相关类型功能具有射态时，才能成功。您可以将输入构建为单独的，索引的数据类型，并允许IDRIS查看构造函数以使用Unification查找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])

预测机器何时会猜测您的意思是依赖类型的编程的重要技能；您会发现自己会通过更多的经验来越来越好。

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