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

*To*: Sam Owre <owre@csl.sri.com>*Subject*: Re: question on dependent typing*From*: Kurt Lichtner <kurt@csg.uwaterloo.ca>*Date*: Wed, 24 Nov 1999 09:09:27 -0500*Delivery-Date*: Wed Nov 24 06:06:40 1999*References*: <199911231944.LAA01953@photon.csl.sri.com>*Sender*: kurt

Sam, 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 BEGIN 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 appreciated, Kurt 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

- Prev by Date:
**Re: question on dependent typing** - Next by Date:
**Re: question on dependent typing** - Prev by thread:
**Re: question on dependent typing** - Next by thread:
**Re: question on dependent typing** - Index(es):