retic blames well typed programs?

[bennn]

Translate this example to the calculus from their POPL'17 paper. What happens?

def dynint()->Dyn:
  return "NaN"

def make_list()->List(Int):
  return [dynint()]

def f(xs:List(Int))->Int:
  return xs[0] + 1

f(make_list())

Running in reticulated:

• it looks like typed code is blaming typed code
• because the error happens inside f
• and make_list is responsible for the value flowing into f

Reading about dereferences (x[0]) in their calculus:

• their blame theorem is that a "safe coercion" never gets blamed. A coercion from type T1 to type T2 is written T1 => T2
• their calculus translates source programs to target programs with coercions and checks. A check is not a coercion. A check that v has type T is written v \Downarrow T
• a bad deference (like our example) raises a blame error
  • that blame error will blame a set of labels
  • the label between typed code for List(Int) => List(Int) will not appear in the set
  • what other labels will? I don't know yet.

NOTE "coercion" and "cast" are my own words, I'm not sure that's exactly what they say in the paper.

[bennn]

Nope no evidence of this