天道酬勤,学无止境

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

I am new to Idris. I am experimenting with types and my task is to make an "onion": a function that takes two arguments: a number and whatever and puts whatever into List nested such number of times.

For example, the result for mkOnion 3 "Hello World" should be [[["Hello World"]]]. I've made such a function, this is my code:

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

The result of program work:

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

This is exactly what I need. But when I do the same, but change Nat to Integer like this

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]

I get an error:

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)

Why does type checking fails?

I think this is because Integer can take negative values and Type can't be computed in case of negative values. If I am right, how does the compiler understand this?

评论

You are right, that the type can't be computed. But that is because the onionListTypeI is not total. You can check this in the REPL

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

(Or even better, demanding %default total in the source code, which would raise an error.)

Because the type constructor is not total, the compiler won't normalize onionListTypeI 0 y to y. It is not total, because of the case onionListTypeI a b = onionListTypeI (a-1) (List b). The compiler does only know that subtracting 1 from an Integer results to an Integer, but not which number exactly (unlike when doing it with a Nat). This is because arithmetic with Integer, Int, Double and the various Bits are defined with primary functions like prim__subBigInt. And if these functions wouldn't be blind, the compiler should have a problem with negative values, like you assumed.

受限制的 HTML

  • 允许的HTML标签:<a href hreflang> <em> <strong> <cite> <blockquote cite> <code> <ul type> <ol start type> <li> <dl> <dt> <dd> <h2 id> <h3 id> <h4 id> <h5 id> <h6 id>
  • 自动断行和分段。
  • 网页和电子邮件地址自动转换为链接。

相关推荐
  • Idris - 自定义依赖数据类型的映射函数失败(Idris - map function on custom dependent data type fails)
    问题 我对 idris 和依赖类型比较陌生,我遇到了以下问题 - 我创建了一个类似于向量的自定义数据类型: infixr 1 ::: data TupleVect : Nat -> Nat -> Type -> Type where Empty : TupleVect Z Z a (:::) : (Vect o a, Vect p a) -> TupleVect n m a -> TupleVect (n+o) (m+p) a exampleTupleVect : TupleVect 5 4 Int exampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: Empty 它是通过添加向量元组归纳构造的,并由每个元组位置的向量长度之和索引。 我试图为我的数据类型实现一个映射函数: tupleVectMap : ((Vect k a, Vect l a) -> (Vect k b, Vect l b)) -> TupleVect n m a -> TupleVect n m b tupleVectMap f Empty = Empty tupleVectMap f (x ::: xs) = let fail = f x in ?rest_of_definition 这会产生以下类型错误: | 20 |
  • 伊德里斯的快速排序(Quicksort in Idris)
    问题 我正在学习 Idris,我想我会尝试为 Vect 类型实现快速排序。 但是我很难使用实用方法,给定一个枢轴元素和一个向量,将向量一分为二,一个元素≤枢轴,另一个元素>枢轴。 这对于列表来说是微不足道的: splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e) splitListOn pivot [] = ([], []) splitListOn pivot (x :: xs) = let (ys, zs) = splitListOn pivot xs in if x <= pivot then (x :: ys, zs) else (ys, x :: zs) *Test> splitListOn 3 [1..10] ([1, 2, 3], [4, 5, 6, 7, 8, 9, 10]) : (List Integer, List Integer) 但是对于 Vect,我需要表达这样一个事实,即两个返回的 Vect 的长度之和等于输入 Vect 的长度。 我显然需要返回一个依赖对。 元素数 ≤ pivot 似乎是第一个值的好候选,但我的第一次尝试: splitVectOn : Ord e => e -> Vect n e -> (k ** (Vect k e, Vect (n - k) e)) 抱怨
  • Quicksort in Idris
    I'm learning Idris and I thought I'd try to implement Quicksort for Vect types. But I'm having a hard time with the utility method that should, given a pivot element and a vector, split the vector in two, one with the elements ≤ pivot and another with those > pivot. This is trivial for lists: splitListOn : Ord e => (pivot : e) -> List e -> (List e, List e) splitListOn pivot [] = ([], []) splitListOn pivot (x :: xs) = let (ys, zs) = splitListOn pivot xs in if x <= pivot then (x :: ys, zs) else (ys, x :: zs) *Test> splitListOn 3 [1..10] ([1, 2, 3], [4, 5, 6, 7, 8, 9, 10]) : (List Integer, List
  • Idris - map function on custom dependent data type fails
    I am relatively new to idris and dependent-types and I encountered the following problem - I created a custom data type similar to vectors: infixr 1 ::: data TupleVect : Nat -> Nat -> Type -> Type where Empty : TupleVect Z Z a (:::) : (Vect o a, Vect p a) -> TupleVect n m a -> TupleVect (n+o) (m+p) a exampleTupleVect : TupleVect 5 4 Int exampleTupleVect = ([1,2], [1]) ::: ([3,4],[2,3]) ::: ([5], [4]) ::: Empty It is inductively constructed by adding tuples of vectors and indexed by the sum of the vector lengths in each tuple position. I tried to implement a map function for my data type
  • Haskell 和 Idris 之间的区别:类型 Universe 中运行时/编译时的反射(Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes)
    问题 因此,在 Idris 中编写以下内容是完全有效的。 item : (b : Bool) -> if b then Nat else List Nat item True = 42 item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A 没有类型签名,这看起来像一种动态类型语言。 但是,确实,Idris 是依赖类型的。 item b的具体类型只能在运行时确定。 当然,这是一个 Haskell 程序员的谈话:Idris 意义上的item b的类型是在编译时给出的, if b then Nat ... 。 现在我的问题是:我的结论是否正确,在 Haskell 中,运行时和编译时之间的边界恰好在值世界(False、“foo”、3)和类型世界(Bool、String、Integer)之间运行,而在 Idris 中,运行时和编译时之间的边界跨越宇宙? 另外,我是否正确地假设即使在 Haskell 中有依赖类型(使用 DataKinds 和 TypeFamilies,参见本文),上面的例子在 Haskell 中也是不可能的,因为 Haskell 与 Idris 相反不允许值泄漏到类型级别? 回答1 是的,您正确地观察到 Idris 中类型与值的区别与仅编译时与运行时和编译时的区别不一致。 这是好事。
  • Idris 可以推断顶级常量类型的索引吗?(Can Idris infer indices in types of top-level constants?)
    问题 例如,Agda 允许我这样写: open import Data.Vec open import Data.Nat myVec : Vec ℕ _ myVec = 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] 并且myVec将按预期具有Vec ℕ 4类型。 但是,如果我在 Idris 中尝试相同的方法: import Data.Vect myVec : Vect _ Nat myVec = [0, 1, 2, 3] 我从类型检查器收到一条错误消息: When checking right hand side of myVec with expected type Vect len Nat Type mismatch between Vect 4 Nat (Type of [0, 1, 2, 3]) and Vect len Nat (Expected type) Specifically: Type mismatch between 4 and len 有没有办法在 Idris 中定义myVec而不手动指定Vect的索引? 回答1 根据评论,Idris 中的顶级漏洞被普遍量化,而不是通过术语推断来填补。 我相信(但是,最终开发团队的某个人必须确认/否认)这样做部分是为了鼓励显式类型,因此是类型导向的开发,部分是为了有一个很好的语法来处理不关心的值接口实现如: Uninhabited
  • In Idris, is “Eq a” a type, and can I supply a value for it?
    In the following, example1 is standard syntax (as documented), with Eq a as a constraint. In example2, I specify Eq a directly as the type of a parameter, and the compiler accepts it. However it is unclear what I can specify as a value of that type. For a specific type a, eg Nat, I assume it would make sense to somehow specify an implementation of Eq Nat, either the default implementation, or some other named implementation. %default total example1: Eq a => (x : a) -> (y : a) -> Type example1 {a} x y = ?example1_rhs example1b: Eq a => (x : a) -> (y : a) -> Type example1b {a} x y = x == y =
  • 在 Idris 中,“Eq a”是一种类型,我可以为它提供一个值吗?(In Idris, is “Eq a” a type, and can I supply a value for it?)
    问题 在下面, example1是标准语法(如文档所述),其中Eq a作为约束。 在example2 ,我直接指定Eq a作为参数的类型,编译器接受它。 但是,尚不清楚我可以指定什么作为该类型的值。 对于特定类型a ,例如Nat ,我认为以某种方式指定Eq Nat的实现(默认实现或其他命名实现)是有意义的。 %default total example1: Eq a => (x : a) -> (y : a) -> Type example1 {a} x y = ?example1_rhs example1b: Eq a => (x : a) -> (y : a) -> Type example1b {a} x y = x == y = True example2: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type example2 a eqa x y = ?example2_rhs example2b: (a : Type) -> Eq a -> (x : a) -> (y : a) -> Type example2b a eqa x y = x == y = True eq_nat : Eq Nat eq_nat = ?eq_nat_rhs example_of_example2 : Type example_of
  • Idris non-trivial type computation for tensor indexing
    I've been messing around with a simple tensor library, in which I have defined the following type. data Tensor : Vect n Nat -> Type -> Type where Scalar : a -> Tensor [] a Dimension : Vect n (Tensor d a) -> Tensor (n :: d) a The vector parameter of the type describes the tensor's "dimensions" or "shape". I am currently trying to define a function to safely index into a Tensor. I had planned to do this using Fins but I ran into an issue. Because the Tensor is of unknown order, I could need any number of indices, each of which requiring a different upper bound. This means that a Vect of indices
  • Haskell 多态递归与组合映射导致无限类型错误(Haskell Polymorphic Recursion with Composed Maps causes Infinite Type Error)
    问题 创建可以动态创建组合地图的函数的正确方法是什么? 这会导致错误(fmap 也会发生): createComposedMaps list = accumulate list map where accumulate (x:xs) m = accumulate xs (m.map) accumulate [] m = m list无关紧要,它只是用来计算乐曲的数量。 我得到的错误是关于“无法构造无限类型”: Occurs check: cannot construct the infinite type: a2 ~ [a2] Expected type: (a2 -> b1) -> a2 -> b1 Actual type: (a2 -> b1) -> [a2] -> [b1] Relevant bindings include m :: (a2 -> b1) -> c (bound at dimensional_filter.hs:166:27) accumulate :: [t1] -> ((a2 -> b1) -> c) -> (a2 -> b1) -> c (bound at dimensional_filter.hs:166:9) In the second argument of ‘(.)’, namely ‘map’ In the second argument
  • Proving if n = m and m = o, then n + m = m + o in Idris?
    I am trying to improve my Idris skill by looking at some of the exercises Software Foundations (originally for Coq, but I am hoping the translation to Idris not too bad). I am having trouble with the "Exercise: 1 star (plus_id_exercise)" which reads: Remove "Admitted." and fill in the proof. Theorem plus_id_exercise : ∀ n m o : nat, n = m → m = o → n + m = m + o. Proof. (* FILL IN HERE *) Admitted. I have translated to the following problem in Idris: plusIdExercise : (n : Nat) -> (m : Nat) -> (o : Nat) -> (n == m) = True -> (m == o) = True -> (n + m == m + o) = True I am trying to perform a
  • Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes
    So in Idris it's perfectly valid to write the following. item : (b : Bool) -> if b then Nat else List Nat item True = 42 item False = [1,2,3] // cf. https://www.youtube.com/watch?v=AWeT_G04a0A Without the type signature, this looks like a dynamically typed language. But, indeed, Idris is dependently-typed. The concrete type of item b can only be determined during run-time. This is, of course, a Haskell-programmer talking: The type of item b in the Idris sense is given during compile-time, it is if b then Nat .... Now my question: Am I right to conclude that in Haskell, the border between the
  • Idris:关于向量串联的证明(Idris: proof about concatenation of vectors)
    问题 假设我有以下 idris 源代码: module Source import Data.Vect --in order to avoid compiler confusion between Prelude.List.(++), Prelude.String.(++) and Data.Vect.(++) infixl 0 +++ (+++) : Vect n a -> Vect m a -> Vect (n+m) a v +++ w = v ++ w --NB: further down in the question I'll assume this definition isn't needed because the compiler -- will have enough context to disambiguate between these and figure out that Data.Vect.(++) -- is the "correct" one to use. lemma : reverse (n :: ns) +++ (n :: ns) = reverse ns +++ (n :: n :: ns) lemma {ns = []} = Refl lemma {ns = n' :: ns} = ?lemma_rhs 如图所示,
  • 我无法用 Idris 证明 (n - 0) = n(I can't prove (n - 0) = n with Idris)
    问题 我试图证明,我认为什么是合理的定理: theorem1 : (n : Nat) -> (m : Nat) -> (n + (m - n)) = m 归纳证明到了我需要证明这一点的地步: lemma1 : (n : Nat) -> (n - 0) = n 当我尝试使用交互式证明器来证明它(为了简单起见,引理)时会发生这种情况: ---------- Goal: ---------- {hole0} : (n : Nat) -> minus n 0 = n > intros ---------- Other goals: ---------- {hole0} ---------- Assumptions: ---------- n : Nat ---------- Goal: ---------- {hole1} : minus n 0 = n > trivial Can't unify n = n with minus n 0 = n Specifically: Can't unify n with minus n 0 我觉得我一定错过了关于减号的定义,所以我在源代码中查找: ||| Subtract natural numbers. If the second number is larger than the first, return 0. total minus
  • 证明如果 n = m 和 m = o,那么在 Idris 中 n + m = m + o?(Proving if n = m and m = o, then n + m = m + o in Idris?)
    问题 我试图通过查看一些练习软件基础来提高我的 Idris 技能(最初用于 Coq,但我希望 Idris 的翻译不会太糟糕)。 我遇到了“练习:1 星(plus_id_exercise)”​​的问题,内容如下: 删除“已录取”。 并填写证明。 Theorem plus_id_exercise : ∀ nmo : nat, n = m → m = o → n + m = m + o. Proof. (* FILL IN HERE *) Admitted. 我已在 Idris 中转换为以下问题: plusIdExercise : (n : Nat) -> (m : Nat) -> (o : Nat) -> (n == m) = True -> (m == o) = True -> (n + m == m + o) = True 我正在尝试逐案分析,但我遇到了很多问题。 第一种情况: plusIdExercise Z Z Z n_eq_m n_eq_o = Refl 似乎工作,但我想说例如: plusIdExercise (S n) Z Z n_eq_m n_eq_o = absurd 但这不起作用并给出: When checking right hand side of plusIdExercise with expected type S n + 0 == 0 + 0 = True
  • 尝试将隐式参数引入 Idris 中定义左侧的范围会导致“is f 应用于太多参数”错误(Trying to bring implicit argument into scope on the left side of a definition in Idris results in "is f applied to too many arguments" error)
    问题 函数applyRule应该提取隐式参数n ,它用于它获取的另一个参数中,类型为VVect 。 data IVect : Vect n ix -> (ix -> Type) -> Type where -- n is here Nil : IVect Nil b (::) : b i -> IVect is b -> IVect (i :: is) b VVect : Vect n Nat -> Type -> Type -- also here VVect is a = IVect is (flip Vect a) -- just for completeness data Expression = Sigma Nat Expression applyRule : (signals : VVect is Double) -> (params : List Double) -> (sigmas : List Double) -> (rule : Expression) -> Double applyRule {n} signals params sigmas (Sigma k expr1) = cast n 不参考{n} ,代码类型检查(如果转换cast n更改为某个有效的双精度)。 但是,添加它会导致以下错误: When checking left hand side of
  • 伊德里斯热切评价(Idris eager evaluation)
    问题 在Haskell,我有可能实现的if是这样的: if' True x y = x if' False x y = y spin 0 = () spin n = spin (n - 1) 这表现得如何我期望: haskell> if' True (spin 1000000) () -- takes a moment haskell> if' False (spin 1000000) () -- immediate 在Racket 中, if像这样,我可以实现一个有缺陷的: (define (if2 cond x y) (if cond x y)) (define (spin n) (if (= n 0) (void) (spin (- n 1)))) 这表现得如何我期望: racket> (if2 #t (spin 100000000) (void)) -- takes a moment racket> (if2 #f (spin 100000000) (void)) -- takes a moment 在伊德里斯,我有可能实现的if是这样的: if' : Bool -> a -> a -> a if' True x y = x if' False x y = y spin : Nat -> () spin Z = () spin (S n) = spin n
  • Can Idris infer indices in types of top-level constants?
    For example, Agda allows me to write this: open import Data.Vec open import Data.Nat myVec : Vec ℕ _ myVec = 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] and myVec will have type Vec ℕ 4 as expected. But if I try the same in Idris: import Data.Vect myVec : Vect _ Nat myVec = [0, 1, 2, 3] I get an error message from the typechecker: When checking right hand side of myVec with expected type Vect len Nat Type mismatch between Vect 4 Nat (Type of [0, 1, 2, 3]) and Vect len Nat (Expected type) Specifically: Type mismatch between 4 and len Is there a way to define myVec in Idris without manually specifying the index of the
  • Trying to bring implicit argument into scope on the left side of a definition in Idris results in "is f applied to too many arguments" error
    The function applyRule is supposed to extract the implicit argument n that is used in another arguments it gets, of type VVect. data IVect : Vect n ix -> (ix -> Type) -> Type where -- n is here Nil : IVect Nil b (::) : b i -> IVect is b -> IVect (i :: is) b VVect : Vect n Nat -> Type -> Type -- also here VVect is a = IVect is (flip Vect a) -- just for completeness data Expression = Sigma Nat Expression applyRule : (signals : VVect is Double) -> (params : List Double) -> (sigmas : List Double) -> (rule : Expression) -> Double applyRule {n} signals params sigmas (Sigma k expr1) = cast n Without
  • Idris: proof about concatenation of vectors
    Assume I have the following idris source code: module Source import Data.Vect --in order to avoid compiler confusion between Prelude.List.(++), Prelude.String.(++) and Data.Vect.(++) infixl 0 +++ (+++) : Vect n a -> Vect m a -> Vect (n+m) a v +++ w = v ++ w --NB: further down in the question I'll assume this definition isn't needed because the compiler -- will have enough context to disambiguate between these and figure out that Data.Vect.(++) -- is the "correct" one to use. lemma : reverse (n :: ns) +++ (n :: ns) = reverse ns +++ (n :: n :: ns) lemma {ns = []} = Refl lemma {ns = n' :: ns} =