notes-computer-programming-programmingLanguageDesign-typeSystemDesignNotes

dons 748 days ago

link

> For instance, Qi's type inferencing engine is Turing complete

Why is that good? Decidability is a nice property of a type system...


Locke1689 747 days ago

link

It's not good, it's very bad. Haskell researchers spent years, in fact, attempting to make sure that it was both decidable and ran in less than exponential time.

The fact that some people actually think an undecidable type system is an advantage is simply an astounding disconnect from reality.


Dn_Ab 747 days ago

link

This is also an issue in Dependent Types. But the case is not as clear cut as you paint it as some argue that the expressibility lost and complexity gained in the system by forcing type checking to terminate is not worth it in practice.

http://www.seas.upenn.edu/~liminjia/research/papers/lambda-e...

(bayle: mb it's this: http://www.andrew.cmu.edu/user/liminjia/research/papers/lambda-eek.pdf "Dependent Types and Program Equivalence")


Locke1689 747 days ago

link

I'm aware of differing opinions, I just think I'm right ;)


njs12345 747 days ago

link

Did they succeed? I vaguely remember a lecture last year where the lecturer told us that type checking in SML was exponential in the worst case ..


Locke1689 747 days ago

link

Type annotations have reduced those cases to very rare instances, but yes there are still cases where the type checker can produce exponential runtime.


there should never be a runtime type error unless:

(i've heard that in C# the typechecker assumes covariance in arrays, e.g. an array of cats is also an array of animals, but the runtime does not in some cases, e.g. if you add a giraffe to an array of cats, that'll typecheck but cause a runtime error (!?!) -- we dont want that)

--

softcrash: throw a stack trace

hardcrash: on some host platforms, same as softcrash; on others, segfault

all crashes should be softcrashes, unless:

note that for all but the first case (external library), a special flag may be passed on the commandline to the compiler to require 'safe mode', in which case the dangerous speed things cant be turned off (mb safe mode can also be per file or per module, in case you trust some of your modules but not others)

--

a type promise is like a typecast a typecast is like an assertion

--

i guess Any should technically be a type that matches any type.

mb we should distinguish between Any, the type that matches any type, and Wildcard, the type of a variable for which typechecking is waived.

E.g. if you pass an Any to a function that requires an Int, that's a compile-time typechecking error, but if you pass a Wildcard to the same function, there is no compile-time error (but the program may softcrash at runtime)

when a type demand is encountered for a variable of type Wildcard, the effect is as if a programmer promise was written at the place of the wildcard declaration which satisfies that type demand. This may require type inference to 'reverse engineer' the original promise when a type demand is encountered after the data has been transformed, e.g. if x is type Wildcard and we pass x to a function, which assumes that its an array and maps another function over that array, and the other function requires Ints, then we infer a type promise at the original Wildcard location that says that x is an array of ints.

this implies that we can have wildcards within a type, e.g. array of wildcard.

an IDE may ask the compiler for a list of all inferred type promises, of course

so things of type Wildcard operate like variables in interpreted languages such as Python

note that if runtime typechecking is turned off, Wildcards may cause a hard crash

Wildcard is the default type. You can do something like 'use strict warn' to turn wildcards into warnings or 'use strict' to turn them into errors

--

need a general way to give the compiler strictness requests for warnings or errors, like 'use strict warn', 'use strict', 'turn off runtime type checking', scopable (e.g. 'use strict but only in this function, or module, or object class definition', similarly with scoped 'turn off runtime type checking')

--

think more about http://en.wikipedia.org/wiki/Covariance_and_contravariance_%28computer_science%29 and more about existence types

--

read http://en.wikipedia.org/wiki/Type_system

--

local vs global type inference: http://lambda-the-ultimate.org/node/2862

--

http://lambda-the-ultimate.org/classic/message6587.html#6615

---