Can I define the general concept of x==y = p(x) == p(y) in Idris?

Question

I want to define a type constructor which embodies the concept of using a type wrapper to define equality on a domain type t1 by projecting onto a domain type t2 with a function p.

The following specific example works, where t1 = ABC, t2 = Nat and p is the function abc_2_nat:

%default total

data ABC = A | B | C

abc_2_nat : ABC -> Nat
abc_2_nat A = 1
abc_2_nat B = 1
abc_2_nat C = 2

data Projected_abc : Type where
  Project_abc : ABC -> Projected_abc

Projected_abc_equals : Projected_abc -> Projected_abc -> Bool
Projected_abc_equals (Project_abc x) (Project_abc y) = abc_2_nat x == abc_2_nat y

Eq Projected_abc where 
  (==) = Projected_abc_equals

But, when I attempt to generalize as follows:

data Projected : t1 -> t2 -> (p: t1 -> t2) -> Type
  where Project : t1 -> Projected t1 t2 p

Projected_equals : Projected t1 t2 p -> Projected t1 t2 p -> Bool
Projected_equals (Project x) (Project y) = ?hole

I get this hole:

- + Main.hole [P]
 `--       phTy : Type
             t2 : phTy
              p : Type -> phTy
             t1 : Type
              x : t1
              y : t1
     --------------------------
      Main.hole : Bool

This doesn't work because it doesn't recognise that p is of type t1->t2 (which is what I want).

I suspect that I'm asking too much to supply the projection function as an argument to a type constructor, and somehow have the projection function available in the scope of the definition of a function whose parameters belong to the constructed type.

Is there any way I can get this to work?

Shersh Shersh · Accepted Answer · 2017-05-15T09:32:57

It's can be done. You Projected generalization is not accurate enough. You should specify types of t1 and t2. Like this:

data Projected : (t1: Type) -> (t2: Type) -> (p: t1 -> t2) -> Type where
    Project : t1 -> Projected t1 t2 p

Without this Idris compiler can't guess what kind of thing are t1 and t2 exactly. One more note: to compare values of type t1 by comparing projections to t2 domain, you should be sure that you can compare values of type t2. Thus general projection equality looks like this:

projected_equals : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool
projected_equals {p} (Project x) (Project y) = p x == p y

And you can write Eq instance for it!

Eq t2 => Eq (Projected t1 t2 p) where
    (==) = projected_equals

And it also works. So if you define something like this:

data ABC = A | B | C

abc_2_nat : ABC -> Nat
abc_2_nat A = 1
abc_2_nat B = 1
abc_2_nat C = 2

You can use your abc_2_nat projection to implement corresponding projector:

abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat
abcNatProjector abc = Project abc

I have to use Main.abc_2_nat to resolve ambiguilty because otherwise abc_2_nat can be any implicit type parameter. Idris has no power to guess what you want. Gladly, compiler helps me with this warning:

Eq.idr:13:37-46:WARNING: abc_2_nat is bound as an implicit
    Did you mean to refer to Main.abc_2_nat?

And now you can check in REPL that it works!

λΠ> abcNatProjector A == abcNatProjector B
True : Bool
λΠ> abcNatProjector A == abcNatProjector C
False : Bool

Bonus addition:

If you mark abcNatProjector as implicit function, like this:

implicit
abcNatProjector : ABC -> Projected ABC Nat Main.abc_2_nat
abcNatProjector abc = Project abc

You can define some fancy operator

infixr 5 ==^
(==^) : Eq t2 => Projected t1 t2 p -> Projected t1 t2 p -> Bool
(==^) = projected_equals

And compare values of type ABC with it without using abcNatProjector explicitly.

λΠ> A ==^ B
True : Bool
λΠ> A ==^ C
False : Bool

Can I define the general concept of x==y = p(x) == p(y) in Idris?

1 Answers