我是伊德里斯的新手。我正在尝试类型,我的任务是制作一个“洋葱”:一个带有两个参数的函数:一个数字和任何东西,并将任何东西放入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
负值时无法计算。如果我是对的,编译器如何理解这一点?
你是对的,类型无法计算。但那是因为onionListTypeI
不是全部。你可以在 REPL 中检查这一点
*test> :total onionListTypeI
Main.onionListTypeI is possibly not total due to recursive path:
Main.onionListTypeI, Main.onionListTypeI
(或者甚至更好,要求%default total
在源代码中,这会引发错误。)
因为类型构造函数不是完整的,所以编译器不会规范化onionListTypeI 0 y
to y
。由于情况原因,这并不完全onionListTypeI a b = onionListTypeI (a-1) (List b)
。编译器只知道从 a 中减去 1Integer
结果到Integer
,但不是确切的数字(与使用Nat
)。这是因为算术与Integer
, Int
, Double
以及各种Bits
定义了主要函数,例如prim__subBigInt
。如果这些函数不是盲目的,编译器应该会遇到负值问题,就像您假设的那样。
本文内容由网友自发贡献,版权归原作者所有,本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容,请联系:hwhale#tublm.com(使用前将#替换为@)