The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

OK, that gets into the details of how type checking on match
statements is done.  In general, in a match statement of the form
match val as val' in (T a b) return (f a b val') with
| const1 arg1 arg2 => ...
| const2 arg1 arg2 => ...
end
there are three type checkings that take place:
First, f a b val' has to type check whenever val' is of type T a b,
and have a value of type either Set, Type, or Prop.
Then, inside each branch of the match, the body of the branch has to
return something of type f a b val' with a, b calculated based on the
constructor arguments (for example, say const1 arg1 arg2 is of type T
(g arg1 arg2) (h arg1 arg2), then the body of the first branch has to
return f (g arg1 arg2) (h arg1 arg2) (const2 arg1 arg2).
Finally, the overall return type of the match statement is calculated
based on the input value; so if val is of type T a0 b0, then the
overall match statement is of type f a0 b0 val.

So, in the original definition of Wrap, the problem was that it wanted
to typecheck "left m" to type Node but since m is of type Element tag,
that expression doesn't typecheck.  But on the other hand, the revised
definition of Wrap could be written more completely as:
match tag as tag' return (Element tag' -> Node) with
| L => fun m0 : Element L => left m0
| R => fun m0 : Element R => right m0
end m.
Here, Element tag' -> Node always makes sense and is of type Set.
Also, the first match body "fun m0 : Element L => left m0" typechecks
to type "element L -> Node"; and similarly for the second match body.
And then the overall match statement has result of type Element tag ->
Node, which you can feed m : Element tag into.
-- 
Daniel Schepler

On Thu, Feb 13, 2014 at 4:26 PM, Kirill Taran 
<kirill.t256 AT gmail.com>
 wrote:
> Daniel,
>
> That really works. But it is not obvious for me, why "fresh" function is
> casted to proper type while given argument isn't.
> What about Cast function, I can't imagine how to tie node and tag together
> yet.
>
> Sincerely,
> Kirill Taran
>
>
> On Fri, Feb 14, 2014 at 4:04 AM, Daniel Schepler 
> <dschepler AT gmail.com>
> wrote:
>>
>> For the definition of Wrap, you need the "convoy pattern" described in
>> CPDT to get m to be the right type inside the match:
>>
>> Definition Wrap {tag} (m : Element tag) : Node :=
>>   match tag return (Element tag -> Node) with
>>   | L => fun m => left m
>>   | R => fun m => right m
>>   end m.
>>
>> (And then, of course, you could optimize that to something like:
>> Definition Wrap' {tag} : Element tag -> Node :=
>>   match tag (* return (Element tag -> Node) *) with
>>   | L => left
>>   | R => right
>>   end.
>> )
>> --
>> Daniel Schepler
>>
>> On Thu, Feb 13, 2014 at 3:47 PM, Kirill Taran 
>> <kirill.t256 AT gmail.com>
>> wrote:
>> > I also tried (not very hard) to invent "opposite" of previous
>> > definition:
>> >
>> > Definition Wrap tag (m : Element tag) : Node :=
>> >   match tag with
>> >   | L => left m
>> >   | R => right m
>> >   end.
>> >
>> > But that fails, too. (Coq expects m to be Element L instead of Element
>> > tag.)
>> > I definetely should to glance at CPDT, but hadn't time for that yet.
>> >
>> > Sincerely,
>> > Kirill Taran
>> >
>> >
>> > On Fri, Feb 14, 2014 at 3:35 AM, Kirill Taran 
>> > <kirill.t256 AT gmail.com>
>> > wrote:
>> >>
>> >> Hello again,
>> >>
>> >> What about such piece of code?
>> >>
>> >> Inductive  Tag := L | R.
>> >> Definition Element tag :=
>> >>   match tag with
>> >>   | L => nat
>> >>   | R => bool
>> >>   end.
>> >> Inductive Node :=
>> >>   | left  : Element L -> Node
>> >>   | right : Element R -> Node.
>> >>
>> >> Definition Cast tag (n : Node) : Element tag :=
>> >>   match tag with
>> >>   | L => match n return Element L with left  e => e end
>> >>   | R => match n return Element R with right e => e end
>> >>   end.
>> >>
>> >> Coq can't infer that there enough branches and complains on definition
>> >> of
>> >> Cast.
>> >>
>> >> Pierre,
>> >>
>> >> I didn't find how to launch code with absurd pattern (!), your example
>> >> doesn't work for me.
>> >> Have I to enable any settings?
>> >>
>> >> Sincerely,
>> >> Kirill Taran
>> >>
>> >>
>> >> On Fri, Feb 14, 2014 at 12:32 AM, Kirill Taran 
>> >> <kirill.t256 AT gmail.com>
>> >> wrote:
>> >>>
>> >>> Daniel,
>> >>> Ow, I didn't try that; thanks.
>> >>>
>> >>> Pierre,
>> >>> Thanks for advices about return and !. By the way, I really noticed
>> >>> that
>> >>> the code I am working on now becomes pretty difficult in the sense
>> >>> that I
>> >>> have to do some manual work.
>> >>> Maybe there are any libs like lenses for haskell? (For reducing
>> >>> boilerplate, when you need to extract something from the bottom of
>> >>> structure
>> >>> with different dependencies.)
>> >>>
>> >>> Sincerely,
>> >>> Kirill Taran
>> >>>
>> >>>
>> >>> On Thu, Feb 13, 2014 at 11:11 PM, Pierre-Marie Pédrot
>> >>> <pierre-marie.pedrot AT inria.fr>
>> >>>  wrote:
>> >>>>
>> >>>> On 13/02/2014 19:54, Kirill Taran wrote:
>> >>>> > But Coq complains about definition of Matching: it says that
>> >>>> > pattern
>> >>>> > matching is non-exhaustive and there are can be branches L right
>> >>>> > and R
>> >>>> > left. But we never can construct such objects. Why Coq can't infer
>> >>>> > that?
>> >>>>
>> >>>> Because this is undecidable in general. You have to write out return
>> >>>> clauses by hand when you start messing with dependent
>> >>>> pattern-matching.
>> >>>>
>> >>>> Or you can use Program to do the dirty job for you.
>> >>>>
>> >>>> Program Definition Matching (n : Node) :=
>> >>>>   match n with
>> >>>>   | L left  => True
>> >>>>   | R right => True
>> >>>>   | _ => !
>> >>>>   end.
>> >>>>
>> >>>> (Here '!' stands for the absurd case. Have a look at the generated
>> >>>> term
>> >>>> to understand how it works.)
>> >>>>
>> >>>> The more your inductives will be dependent, the more you will need to
>> >>>> do
>> >>>> things by hand. I recommend the reading of CPDT to get a handful of
>> >>>> neat
>> >>>> design patterns when programming with dependent types.
>> >>>>
>> >>>> PMP
>> >>>>
>> >>>>
>> >>>
>> >>
>> >
>
>