Idris：函数与 Nat 参数一起使用，但无法通过 Integer 参数进行类型检查

Question

我是 Idris 的新手。我正在试验类型，我的任务是创建一个 "onion": 一个函数，它有两个参数：一个数字和任何东西，并将任何东西放入 List 嵌套了这么多次。

例如，mkOnion 3 "Hello World" 的结果应该是 [[["Hello World"]]]。我做了这样一个功能，这是我的代码：

onionListType : Nat -> Type -> Type
onionListType Z b = b
onionListType (S a) b = onionListType a (List b)

mkOnionList : (x : Nat) -> y -> onionListType x y 
mkOnionList Z a = a
mkOnionList (S n) a = mkOnionList n [a]

prn : (Show a) => a -> IO (); 
prn a = putStrLn $ show a;

main : IO()
main = do
    prn $ mkOnionList 3 4
    prn $ mkOnionList 2 'a'
    prn $ mkOnionList 5 "Hello"
    prn $ mkOnionList 0 3.14

程序运行结果：

[[[4]]]  
[['a']]  
[[[[["Hello"]]]]]  
3.14

这正是我需要的。但是当我这样做时，但是像这样将 Nat 更改为 Integer

onionListTypeI : Integer -> Type -> Type
onionListTypeI 0 b = b
onionListTypeI a b = onionListTypeI (a-1) (List b)

mkOnionListI : (x : Integer) -> y -> onionListTypeI x y 
mkOnionListI 0 a = a
mkOnionListI n a = mkOnionListI (n-1) [a]

我得到一个错误：

When checking right hand side of mkOnionListI with expected type   
    onionListTypeI 0 y

Type mismatch between  
    y (Type of a) and   
    onionListTypeI 0 y (Expected type)

为什么类型检查失败？

我认为这是因为 Integer 可以取负值，而 Type 在负值的情况下无法计算。如果我是对的，编译器是怎么理解的？

Answer 1

你是对的，类型无法计算。但那是因为 onionListTypeI 不是总的。您可以在 REPL

中查看

*test> :total onionListTypeI
Main.onionListTypeI is possibly not total due to recursive path:
    Main.onionListTypeI, Main.onionListTypeI

（或者更好，在源代码中要求 %default total，这会引发错误。）

因为类型构造函数不是总的，编译器不会将 onionListTypeI 0 y 规范化为 y。它不是总数，因为大小写 onionListTypeI a b = onionListTypeI (a-1) (List b)。编译器只知道从 Integer 中减去 1 得到 Integer，但不知道具体是哪个数字（与使用 Nat 时不同）。这是因为 Integer、Int、Double 和各种 Bits 的算术是用 prim__subBigInt 等主要函数定义的。如果这些函数不是盲目的，编译器应该会遇到负值问题，就像您假设的那样。

Idris：函数与 Nat 参数一起使用，但无法通过 Integer 参数进行类型检查

Idris: function works with Nat parameter and fails type checking with Integer parameter

partial-functions

idris