Too restrictive i.e.
($\lambda$ r:{x:Nat}. r.x) {x=0,y=1}
Let's express this in OCaml, well, OCaml actually doesn't support record subtying
type xt = {x:int}
type xyt = {x:int; y:int}
let f (r:xt) = r.x
let vxt = {x=1}
let vxyt = {x=2; y=3}
f vxt (* ok *)
f vxtt (* not ok ... *)
S is a subtype of T written S <: T, mean any term of type S can safely be used in a context where a term of type T is expected
$$\frac{\Gamma \vdash t : S \quad S <: T}{\Gamma \vdash t : T} \quad\quad \textbf{(T-SUB)}$$Since function can be passed as argument, we must also give a subtyping rule for function types
$$\frac{T_1 <: S_1 \quad S_2 <: T_2}{S_1 -> S_2 <: T_1 -> T_2} \quad\quad (\textbf{S-ARROW})$$Example
TODO: still can't find a good example
let f1 = $\lambda$ r:{x:Nat}. {x=r.x, y=r.x}
{x:Nat} -> {x:Nat, y:Nat}
let f2 = $\lambda$ r:{x:Nat, y:Nat}. {x=r.x}
{x:Nat, y:Nat} -> {x:Nat}
f1 <: f2
let r2 = f2 {x=1, y=2}
let r2' = f1 {x=1, y=2}
// NOTE: kind of figure out the S-ARROW now, but still no concrete example that you can be found in OO language
// argument {x:Nat, y:Nat} is subtype of what f1 is expecting, so you can apply
// return {x:Nat, y:Nat} is subtype of what people calling f2 is expecting, so they can use the returned value safelyhttp://lampwww.epfl.ch/teaching/archive/type_systems/2004/slides/5.pdf the image is really good
from wiki Covariance and contravariance (computer science)
For example in OCaml, "list of Cat" is a subtype of "list of Animal" because the list constructor is covariant, while "function from Animal to String" is a subtype of "function from Cat to String" because the function type constructor is contravariant in the argument type
don't quite get the arithmic implementation .... only knowing it is because the direct use of the specified subtyping is hard to use in real type checker .... also the course from epfl has scala implementation (and their course at 2004 seems to have so few people ...)
also have an example on s-arrow, for Int -> Int
also they use euler diagram to visualize it https://en.wikipedia.org/wiki/Euler_diagram
the funnel example is great ! As this was all rather counter-intuitive, @jcoglan suggested an analogy: funnels.
Finally, @tomstuart closed the meeting by summarising an important point about the tricksy S-Arrow:
When I have taught this before, people often make the mistake of thinking that functions are now contravariant in their argument types and covariant in their return types: this is not what the chapter is saying. (As S-Arrow describes the substitutability of entire function types, i.e. when can you replace some type T → T with another, not just the substitutability of argument types and return types in general. To use our funnel analogy, we're not talking about substituting the input and output of the funnel, we're talking about substituting the funnel itself.
I think I finally get it the confusion is mix abstraction (function) with application (calling function)
($\lambda$ r:{x:Nat} r.x) {x=1}
($\lambda$ r:{x:Nat} r.x) {x=1, y=1}
in the above, we think we can pass subtype as function argument, so for S-Arrow, if we are still thinking about parameter along, we get the wrong idea
In [ ]: