The Coq mailing list

[Bas Spitters <b.a.w.spitters AT gmail.com>]

Not a precise answer to your question, but ever since the introduction
of type classes, the type class of coercions between two types has
been a standard example,
In haskell:
https://homepages.inf.ed.ac.uk/wadler/papers/class/class.dvi
In our math-classes:
http://dx.doi.org/10.1017/S0960129511000119
In lean, coercions are even managed using type classes (IIUC). Sec 4 here:
https://arxiv.org/abs/2001.04301
They claim their algorithms can be ported to Coq, and would solve some
of the problems we are experiencing.

On Sat, Feb 29, 2020 at 5:27 PM Gregory Malecha 
<gmalecha AT gmail.com>
 wrote:
>
> Hello --
>
> It makes sense that it increases the size of the search space for CS. It 
> sounds like the answer is that it isn't possible, and that the correct 
> thing to do is to write all of the instances that you need.
>
> Thanks.
>
> On Sat, Feb 29, 2020 at 11:07 AM Beta Ziliani 
> <beta AT mpi-sws.org>
>  wrote:
>>
>> Sounds like that would bloat the search space of CS. In this case is 
>> obvious, but how do you foresee if you need some coercion (and which one!)?
>>
>> Written from mobile. Excuse my limited communication.
>>
>> On Sat, Feb 29, 2020, 11:39 AM Gregory Malecha 
>> <gmalecha AT gmail.com>
>>  wrote:
>>>
>>> Hello --
>>>
>>> Is there a way to get canonical structures and coercions to work 
>>> together? Here's my toy example:
>>>
>>> Structure EX : Type :=
>>> { t :> Type
>>> ; GET : t -> Prop }.
>>>
>>> Definition foo {e : EX} := e.(GET).
>>>
>>> Canonical Structure TrueEX : EX :=
>>>   {| GET := fun _ : bool => true |}.
>>>
>>> Definition to_bool (n : nat) :=
>>>   match n with
>>>   | 0 => false
>>>   | _ => true
>>>   end.
>>>
>>> Coercion to_bool : nat >-> bool.
>>>
>>> Check (foo true). (* works great! *)
>>> Check (foo 1).    (* fails *)
>>>
>>> Intuitively, I would expect the term [@foo boolEX (to_bool 1)] but 
>>> instead I get a type error "the term 1 has type nat while it is expected 
>>> to have type EX".
>>>
>>> Is there some way to make this work without making instances for, e.g. 
>>> [natEX], which is the composition of [to_bool] and [foo]?
>>>
>>> Thanks.
>>>
>>> --
>>> gregory malecha
>>> gmalecha.github.io
>
>
>
> --
> gregory malecha
> gmalecha.github.io