C0t and Static Semantics

Hello,

Regarding Subsection 6.6 “A Simple Type System (C0t)”, I would like to refer to 5 points:

  1. §6.6: Typo (&x should be *x).

image


  1. §6.6.1 after Def 6.6.6: some rule names do not match with those in the definition: e.g. [CmpPtr] vs [PtrCmp]. The rule [Cmp] is missed.
    image

image


  1. §6.6.2 in Def 6.6.7: Typo [Abort] rule:
    image

  1. §6.6.9: in this example, I have 2 questions:
  • Are we indeed able to give (or are we allowed to guess) the types of all statement and expression although they relay on ill-typed expression?
  • If Answer is No, would it make more sense if we got the error in the primse of [Indir] (where x shouldn’t be char) instead of [Var] since the rule [Var] infers the type well?

image


  1. §6.6.10: Some typos

image

Most of your points are correct.

Regarding this: The first answer is no – you can not derive any type for ill-typed expressions.

The relation \vdash is interesting since, for fixed environment and expression, you get at most one type (proof: exercise).

Now, for the term and environment from the example, you can not find any such type. In other words, \forall t.\,\neg (\Gamma \vdash e : t.

Think about how you prove this. You are given an arbitrary derivation, and need to derive a contradiction. By sharply looking at the derivation, you can see that it must derive type int, since the only syntactically applicable typing rule [Arith] enforces this. This process is called inversion, and also tells us that there must be sub-derivations which derive int for the subterms. If we continually “invert” these sub-derivations, we eventually find that \Gamma\,x = \texttt{char*}, which contradicts \Gamma\,x=\texttt{char}. This justifies claiming that this rule is wrong.

When constructing this derivation (i.e. when writing a compiler), the error would be reported one rule further down, at [Indir], since (as you mentioned) x has a valid type. This is because of typing uniqueness – it suffices to propagate the type from the smaller terms to the larger terms. If we did not have typing uniqueness (like in the OCaml type system, which has polymorphism), it would be rather hard to even say which rule is wrong, since there is non-local interaction happening between the typing rules.

To a limited extend, this already happens here, where you can argue that since [Var] supplies the wrong type to [Indir], both are wrong in combination.

To summarize, you should always explain what exactly goes wrong when showing that something can not be typed. Usually, there is no one precise rule, since deriving a type only becomes impossible when combining multiple rules such that they together are contradictory, while no single rule is in isolation.

CC @hack for the other typos.

1 Like

The typos are fixed now. Thanks.

Note:
You can hover slightly left of a paragraph to get a permalink to that paragraph.
Example:
Subsection 6.6.1: Expressions
Screenshot_20220706_073455

1 Like