proj-oot-old-150618-ootType

toread

erlang success types:

http://www.it.uu.se/research/group/hipe/papers/succ_types.pdf

http://user.it.uu.se/~tobiasl/publications/contracts.pdf

mb http://users.dsic.upv.es/~jsilva/papers/PEPM2013.pdf

mb http://artemis-new.cslab.ece.ntua.gr:8080/jspui/bitstream/123456789/5300/1/DT2010-0190.pdf

typescript:

http://cs.au.dk/~amoeller/papers/tajs/paper.pdf

http://www.quora.com/Scala/Why-cant-Scala-infer-the-type-of-recursive-functions

Pierce's types book

"

design todos

oot type system design principals

design principal "everything is an interface": a later programmer should always be able to make use of a library with a type of data which was unanticipated by the library, but which obeys the same signature in all public methods as the data type that the library was built for (e.g. a parser that is written to work with a string-as-linked-list datatype should also work with a bytestring data type, even if bytestrings weren't invented until later)

type system modules

type inference

module-local type inference. Note that this is different from 'local type inference' as usually defined.

success typing

optional 'type system modules' that allow programmers to have stronger type systems for particular modules or sets of modules.

hybrid type checking: runtime type checking except when compiler said it was ok

allow programmer to give 'assumptions'

the variadic haskell problem

See the relevant section in ootTypeNotes1.

Current best guess solution:

initial compiler path to resolve ad-hoc polymorphism in return types, in which only local type inference (in the conventional sense of the term; e.g. even recursion on a single function is not followed) is used; after this, normal two-way constraint propagation is used, however, ad-hoc polymorphism in return values cannot be resolved anymore for the purpose of typechecking. By "for the purpose of typechecking" i mean that an implementation can be chosen, but that the type signature cannot be specialized to this implementation, so other parts of the program must typecheck as if the choice of implementation were unknown.

note that this doesn't apply to parametric polymorphism

extensible type system

type system as a library. Building on the idea that type checking is often specified as inference rules which are of the form "from this, you may derive that"

co/contravariance, subtyping, promise/demand, failure and success typings

Provide the programmer facilities to make type constraints that are either "sufficient" or "necessary". Sufficient and necessary are modes that can be attached to any explicit or implicit type annotation. A sufficiency constraint asserts that if its conditions are satisfied, then there will not be a type error at runtime. A necessary constraint asserts that if its conditions are NOT satisfied, then there WILL be a type error at runtime (in at least some cases).

Traditional type annotations are all sufficiency constraints. Traditional compilers will only compile if they can prove sufficiency for every value, that is, if they can prove that in no case will there be a type error at runtime.

Oot operates this way in 'strict mode', however, outside of strict mode, Oot will accept programs for which it cannot be sure that there will be no runtime time errors (in this case, Oot inserts runtime type checks). However, Oot will still reject programs for which it can prove that there is a type error; that is, for which it can prove that some necessary type constraint cannot be fulfilled.

Even where the programmer does not provide type constraints, they are often inferred.

In more detail:

Each term corresponds to two places where type constraints may be applied; its 'lefthand' and its 'righthand', corresponding to input and output (we say 'lefthand' and 'righthand' to lessen confusion because the input and output of a function are each their own terms).

Any term for which the type is determined has both a necessary and a sufficient type constraint of that type at both lefthand and righthand. For instance, any occurrence of the literal 3 has a necessary type constraint of Int and also a sufficient type constraint of Int at both lefthand and righthand.

For each of sufficiency and neccesity: Its lefthand is unified by finding all of the places that provide values to that term, and taking the union of their type constraints. For each of sufficiency and neccesity: Its righthand is unified by finding all of the places to which that term provides values, and also any programmer-given type constraints on this term, and taking the intersection of their type constraints. For each of lefthand and righthand: the sufficiency constraints are replaced by their intersection with the neccesity constraints.

(note: when we say to take the union or intersection, should we allow arbitrary anonymous union and intersection types to be implicitly created? or should we only look on the lattice of types explicitly created by the programmer? i'm in favor of the latter, to reduce computational complexity; i have a feeling that the unrestricted problem could be NP-complete)

For each of sufficiency and neccesity: if at any term, the term's lefthand is a subtype of its righthand, then the constraint is considered fulfilled at that term.

Propagate the constraints.

If the compiler calculates that a neccessary type constraint is unfulfilled at any term, the compiler halts with a type error.

If the compiler calculates that a sufficiency type constraint is unfulfilled at any term, the compiler continues but inserts a runtime type check at that location.

A subtype inherits all righthand sufficient and necessary type constraints of its righthand supertype.

If a subtype has a sufficiency constraint which is a proper subset of the sufficiency constraint of its supertype, that is a type error. This can only occur when improper demands are made on the subtype which conflict with the sufficiency constraints of its supertype. (note/todo: how can the programmer control/avoid unwanted implicitly inferred sufficiency constraints on the supertype?)

The type of input to a multiple dispatch function is determined to be the disjunction of all input types defined in the dispatch cases (e.g. this disjunction forms both a necessary and a sufficiency constraint). (note: this means that if the dispatch cases can be found in multiple places in the source, they must all be gathered before type checking. If the user wants the program to compile despite leaving out some of the cases, they can add a default dispatch case).

For example, if you have a function 'f x = x + 4', and +: Num a => a -> a -> a, and a subtype of Int is "3", and 3 \member 3, and you do y = f 3, and also z = f 4, then:

the left side of the input to f is unified with 3 and 4. The union of these types is Int. The right side is unified with the input to +, namely, Num a => a. The left side of the output of f is unified with the right side of the input to +, namely, Num a => a. The right side is unified with y, which is Any.

(todo also show how left/right side of plus is calculated, and how it allows specialization of Int)

So at each term, the type checking is fulfilled. However, i don't see yet which of these inferred type represent the inferred types that we want to show to the user; i'd say we want to get a=Int on f's input, and Num a => a on f's output, giving us f: Int -> Int. But really shouldn't it just be f: Num a => a -> a?

perhaps we should always preferentially define functions by their implementation where possible? So we'd take the righthand side of f's input and the lefthand side of its output, yielding f: Int -> Int.

---

there is a whole other meaning of 'promise' vs 'demand':

an assertion in the typical sense means 'please check at runtime if this is true'. translated to compile time, this is a property such as 'immutable', where you are saying, 'compiler, prove at compile time that this is true'. these are runtime and compile-time demands. But oot also wants to allow compile-time promises, that is, assumptions, that is, "compiler, i promise that this is true, you may assume this for the purpose of proving that other things are true".

run-time promises i guess are things like 'you can omit bounds-checking on this array in this function'

so i guess we have three ortho dimensions here: sufficiency/necessity,runtime/compiletime, promise/demand

--

type system should include types (which specify domains and ranges of partial functions), properties (like 'total on its domain', 'injective', 'associative', 'functional relation', "antisymmetric relation", 'monotone'), and what you are allowed to do (copyable vs. only movable, immutable)

--

i guess an 'interface' is:

an "abstract semantic" is something such that two functions with the same "abstract semantic" return the same values as each other when given any finite input