1

私はイドリスが初めてです。私は型を実験していますが、私の仕事は「タマネギ」を作ることです.2つの引数を取る関数です：数値と何でも、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負の値の場合は計算できないためだと思います。私が正しければ、コンパイラはこれをどのように理解しますか?

4

1 に答える 1

2

その通り、型は計算できません。しかし、それは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です。そして、これらの関数がブラインドではない場合、コンパイラは、あなたが想定したように、負の値に問題があるはずです。

于 2016-05-27T19:16:18.657 に答える