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

Re: question on dependent typing

Thank you for the quick help.  Your solution fixed it but uncovered
another similar typing issue in my actual spec.  The following is the
same example as my previous one, but I have a function f with a domain
dependent on a dependent type.   I've tried quite a few different
alternatives for the type of the domain of  'f' but I'm not satisfying
the typechecker.

t1  : THEORY


  a_type  : type = [#
                  b : setof[int],
                  c : setof[(b)],
                  f : [(c)->int]

d   : var int
t   : var a_type

add(d,t) : a_type = t with [b := add(d, t`b),
                            c := lambda (x:(add(d, t`b))) : t`b(x)
END t1

Again, any insight you can shed into the type of 'add(d,t)`f ' is

Sam Owre wrote:

> 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