0
$\begingroup$

In reading idris code, I sometimes wondered what's the mysterious type constraint =>.

It's said that dependent types are a first-class member of Idris. So can be we express type constraints such as Eq a => Ord a as some kind of function type in the function space ?? -> ??? (here a function mapping a Eq to an Ord). Why do we need a separate operator?

The reason I ask is the small test below that I blundered into. If I declare a function test with an auto-implicit argument and then load it:

test: {auto flag : Int} -> Int
test = ?test_rhs

Instead of showing the original type, Idris2 (as of 0.7.0) will display be type of test as if it's a type constraint:

:t test
Idris.Main.test : Int => Int

Is this a coincidence in syntax, or is it the case that fundamentally in dependent types, type constraints are a special form of implication -> (i.e. auto-implicits)?

If the latter case, how can one write parameterized things such as Eq a => Ord a as an implication (->) form?

-- Update --

It seems that type constraints are exactly auto-implicit arguments with quantity 1.

Among the following three forms of implicit arguments, only the first one is treated as a type constraint Eq a => Ord a:

test1 : {auto x : Eq a} -> Ord a

test2 : {x : Eq a} -> Ord a

test3 : {auto 0 x: Eq a} -> Ord a

The others are shown as normal implicit arguments:

:t test1
Idris.Main.test1 : Eq a => Ord a
:t test2
Idris.Main.test2 : Ord a
:t test3
Idris.Main.test3 : {auto 0 _ : Eq a} -> Ord a
$\endgroup$
2
  • $\begingroup$ It might be worth learning about and comparing with Agda's instance arguments. There, it's made quite obvious that instance arguments elaborate to ordinary arguments (i.e, passing first class records around). $\endgroup$
    – James Wood
    Feb 5 at 10:27
  • $\begingroup$ @JamesWood Thanks for the pointers. I'll have to learn Agda one of these days. $\endgroup$
    – tinlyx
    Feb 7 at 3:29

1 Answer 1

2
$\begingroup$

From the point of view of logic, implicit arguments are indeed just arguments. In that sense, Eq a => Ord a is the same as the function space Eq a -> Ord a.

Always spelling out all arguments can be tedious, so as a programming language it's convenient to be able to elide some arguments as long as they can be inferred by some mechanism. You then need some notation to distinguish explicit from implicit arguments, that's why there are different arrows -> and =>.

$\endgroup$

Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.