[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: question on dependent typing



Kurt,

TCCs of the form "FORALL ... IFF ... " are usually, as in this
case, due to a domain mismatch.  What is going on is that t`c
is of type [(b) -> bool], whereas add(d,t)`c needs to be of
type [(add(d, t`b)) -> bool].  The type system insists that
these domains be the same, and you get the TCC.

You can fix this by including the update to c at the same
time, e.g., either

add(d,t) : a_type = t with [b := add(d, t`b),
                            c := {x: (add(d, t`b))| t`b(x)}]

or, since all the fields are being updated,

add(d,t) : a_type = (# b := add(d, t`b),
                       c := {x: (add(d, t`b))| t`b(x)} #)

If the typechecker knew that (t`b) was a subtype of (add(d, t`b)), 
then you would not get the TCC, as the typechecker would
insert the extend_bool conversion automatically.
Unfortunately, the judgement facility does not currently
support this form of subtype judgement, as there would be a
free variable on the right-hand side.  We plan on exploring
such extensions in the future, though they may slow down
typechecking too much to be incorporated into the system.

Regards,
Sam Owre

> Hi,
> The following spec gives what appears to be an unprovable TCC:
> 
> t1  : THEORY
> 
>   BEGIN
> 
>   a_type  : type = [#
>                   b : setof[int],
>                   c : setof[(b)]
>                #]
> 
> d   : var int
> t   : var a_type
> 
> 
> add(d,t) : a_type = t with [b := add(d, t`b)]
> 
> END t1
> 
> ... and yields:
> 
> % Subtype TCC generated (at line 16, column 20) for  c(t)
>   % unfinished
> add_TCC1: OBLIGATION
>   FORALL (d, t): FORALL (x: int): t`b(x) IFF add[int](d, t`b)(x);
> 
> I'm unsure why I'm getting this.   Can anyone shed some insight?
> 
> Thanks very much in advance,
> Kurt