2

I have encountered a problem with some code I am trying to write in Idris 2. I would like to resolve this issue, but more importantly, I wish to understand it more deeply and develop some skills in diagnosing such issues in general.

I have distilled the problem to the following relatively trivial example:

data D : Nat -> Type where
  V : (n : Nat) -> D n

d : (n : Nat) -> D n
d n = V n

f : D n -> String
f (V n) = show n

t : Nat -> String
t = f . d

The definition of t fails type checking with the following output:

Error: While processing right hand side of t. Can't solve constraint between: ?n [no locals in scope] and n.

Test:11:9--11:10
 07 | f : D n -> String
 08 | f (V n) = show n
 09 | 
 10 | t : Nat -> String
 11 | t = f . d

Some experimentation has revealed that the following alternative definitions for t also fail type checking:

t : Nat -> String
t n = (f . d) n

t : Nat -> String
t = \n => (f . d) n

While these alternatives type check successfully:

t : Nat -> String
t n = f (d n)

t : Nat -> String
t = \n => f (d n)

I am endeavouring to learn Idris (for the second time), and so while I could move on with the definitions which don't involve function composition, I would like to improve my understanding.

It seems to me that the definitions which pass type checking are simply syntactic alternatives with identical semantics and behaviour, and I don't understand why the function composition definitions fail type checking. I would also like to understand the particular error message the type checker reports, so that I can deepen my understanding and resolve similar type checking errors in the future.

I have a few broad questions:

  • How should I interpret the error reported by the type checker in this example, and how can I gather more information about the ?n and n types mentioned? I particularly welcome any advice or tips on how to go about understanding and resolving such an error (teach a man to fish, as the saying goes).
  • Why do the definitions involving function composition fail type checking?
  • What is the best solution for this example? Should I just use a definition which does not involve function composition? Is there a better alternative?
Improve this question

1 Answer 1

Reset to default
1

Let look at the types involved

Prelude.. : (b   -> c     ) -> (a        -> b   ) -> a -> c
f :          D n -> String
d :                             (n : Nat) -> D n

The problem is:

(a        -> b   )
(n : Nat) -> D n

cannot be unified because (a -> b) does not allow the value of the argument to determine the type of return value.

Improve this answer
Sign up to request clarification or add additional context in comments.

6 Comments

Ah, I see. I had assumed it should work, since though b is not a, it will still accept a function for which they are the same. My understanding coming from other functional languages is that a -> b applies no constraint to b in relation to a - they can be different types or the same type. So I expected it to accept any function. But I guess dependent types introduces a different set of possibilities.
Does this then imply that function composition and actually many other common concepts, such as map of Functor, are constrained to functions which do not have dependent return types?
@label17 your understanding is correct
Yes, I receive the same error when trying to define: s : List String as s = map f $ map d [1 .. 3]. And further, when trying to define a function m : Vect k Nat -> Vect k (D ?) the problem reveals itself more clearly. It is not possible to define the value on which the type D depends in the resulting type, since it would be different for each element of the vector, which does not satisfy the type.
@label17 SO isn't suited to longer conversations. Can we continue this in the Idris Discord discord.gg/UX68fDs2jc ?
|

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.