CODEWITHSUNDEEP
dependent-typeidris
Rodrigo Ribeiro
Rodrigo Ribeiro

Reputation: 3218

Constraining a function type with an Idris interface

I'd like to create a function with type constrained by an interface. My intention is to build a simple monoid solver using VerifiedMonoid defined inClasses.Verified module from contrib package.

Idris gives me the following error:

 Monoid-prover.idr line 29 col 5:
 When checking type of MonoidProver.eval:
 Can't find implementation for VerifiedMonoid a

for the type signature of eval:

eval : VerifiedMonoid a => Expr n -> Env a n -> a

Am I doing something silly or missing something? Such constrained types (like eval's type) can be interpreted like Haskell's types?

The complete code is shown below.

module MonoidProver

import Classes.Verified

import Data.Fin
import Data.Vect

%default total

infixl 5 :+:

data Expr : Nat -> Type where
   Var  : Fin n -> Expr n
   Id   : Expr n
   (:+:) : Expr n -> Expr n -> Expr n

Env : VerifiedMonoid a => (a : Type) -> Nat -> Type
Env a n = Vect n a

eval : VerifiedMonoid a => Expr n -> Env a n -> a
eval (Var i) env    = index i env
eval Id      env    = neutral
eval (e :+: e') env = eval e env <+> eval e' env

Upvotes: 2

Views: 251

Answers (1)

Lucy Maya Menon
Lucy Maya Menon

Reputation: 1590

As @Cactus mentioned in a comment, the problem here is that the type signature for Env is not correct. Specifically, since the constraint is on the value of the argument, it is a dependent (pi) type, and Idris enforces that dependent types go left-to-right (be introduced before they are used). My understanding is that basically the compiler will see the argument x : a as being shorthand for \Pi_{(x\;:\;a)}B(x), where B(x) is the part of the type signature to the right of the quantifier. This means that (a : Type) actually binds a fresh a, which is not the same a that was used in the VerifiedMonoid a constraint (which is implicitly universally bound).

Luckily, since Idris isn't Haskell (where all type class constraints must be at the head of the type signature), this is easy to fix: just change your type signature to Env : (a : Type) -> VerifiedMonoid a => Nat -> Type, so that a is bound before it is used!

Upvotes: 1

Related Questions