archives

Bottom Types

I was having a discussion about typing with shelby3 regarding typing in our scripting language, and shelby3 made the following statement:

In an eager, CBV type system, then the type of Nil has to be subsumable to any instantiable type of List otherwise you will have unsoundness. Period.

I am reasonably sure, as I can have an eager language, which is call-by-value, and have strict typing, no sybtyping and no variance, and it will be sound.

Why do we both see this so differently?