What is a type error?

[Joachim Durchholz]

Marshall schrieb:
> Joachim Durchholz wrote:
>> Chris Smith schrieb:
>>> For example, I wrote that example using variables of type int.  If we
>>> were to suppose that we were actually working with variables of type
>>> Person, then things get a little more complicated.  We would need a few
>>> (infinite classes of) derived subtypes of Person that further constrain
>>> the possible values for state.  For example, we'd need types like:
>>>
>>>     Person{age:{18..29}}
>>>
>>> But this starts to look bad, because we used to have this nice
>>> property called encapsulation.  To work around that, we'd need to
>>> make one of a few choices: [...] (c) invent some kind of generic
>>> constraint language so that constraints like this could be expressed
>>> without exposing field names. [...] Choice (c), though, looks a
>>> little daunting.
>> That's not too difficult.
>> Start with boolean expressions.
>> If you need to check everything statically, add enough constraints that
>> they become decidable.
> 
> I'm not sure I understand. Could you elaborate?

Preconditions/postconditions can express anything you want, and they are 
an absolutely natural extensions of what's commonly called a type 
(actually the more powerful type systems have quite a broad overlap with 
assertions).
I'd essentially want to have an assertion language, with primitives for 
type expressions.

>> For the type language, you also need to add primitives for type
>> checking, and if the language is stateful, you'll also want primitives
>> for accessing earlier states (most notably at function entry).
> 
> Again I'm not entirely clear what this means. Are you talking
> about pre/post conditions,

Yes.

Regards,
Jo