I had a few types and definitions like:

```
Inductive type : Set :=
| Nat.
Definition typeDenote (t:type) : Set :=
match t with
| Nat => nat
end.
Inductive binop : type -> type -> type -> Set :=
| Plus : binop Nat Nat Nat
| Fn : forall (t1 t2 t3:type),
((typeDenote t1) -> (typeDenote t2) -> (typeDenote t3))
-> binop t1 t2 t3.
Arguments Fn {t1 t2 t3}.
Definition binopDenote {t1 t2 t3:type} (b:binop t1 t2 t3)
: (typeDenote t1) -> (typeDenote t2) -> (typeDenote t3) :=
match b with
| Plus => plus
| Fn f => f
end.
```

This sort of works.

```
Check @Fn Nat Nat Nat (fun (x y:nat)=>x).
(*
Fn (fun x _ : nat => x)
: binop Nat Nat Nat
*)
Compute (binopDenote (@Fn Nat Nat Nat (fun (x y:nat)=>x))) 3 2.
(*
= 3
: typeDenote Nat
*)
```

But could there be a way to have the `Nat Nat Nat`

passed to `Fn`

as implicit arguments?

So that I can do:

```
Compute (binopDenote (Fn (fun (x y:nat)=>x))) 3 2.
```

The `Nat Nat Nat`

can be inferred from the type of the function passed as argument to `Fn`

, right? Is it not so?

You can use canonical structures but my approach seems awkward and relies on equality proofs and explicit rewriting. Somebody else can probably come up with a more reasonable approach.

```
Structure type' :=
{ #[canonical=no] type'_type :> type;
typeDenote' : Set;
#[canonical=no] typeDenote'_ok : typeDenote type'_type = typeDenote';
}.
(* [eq_refl] must be transparent here. *)
Canonical Structure type'_nat := {| type'_type := Nat; typeDenote' := nat; typeDenote'_ok := eq_refl |}.
Definition Fn' {t1 t2 t3 : type'} : (typeDenote' t1 -> typeDenote' t2 -> typeDenote' t3) -> binop t1 t2 t3 :=
match typeDenote'_ok t1 in _ = T1, typeDenote'_ok t2 in _ = T2, typeDenote'_ok t3 in _ = T3 return
(T1 -> T2 -> T3) -> _
with
| eq_refl, eq_refl, eq_refl => Fn
end.
Check Fn' (fun (x y:nat)=>x).
Compute (binopDenote (Fn' (fun (x y:nat)=>x))) 3 2.
```

Last updated: Feb 04 2023 at 21:02 UTC