3 ms·

I meant "expressiveness" purely in the sense that "we can write more programs 'without' types than with them" (of course, the types are 'still in there somewher

I meant "expressiveness" purely in the sense that "we can write more programs 'without' types than with them" (of course, the types are 'still in there somewhere'; we're just ignoring them). I wasn't referring to external tooling, which I agree gains a lot from strong types (specifically because a load of programs have been forbidden, which makes their job tractable). When dependent types and proving correctness are mentioned, there is often an assumption that some magical ability is gained. For example, all the questions here about error handling. Dependent types don't handle errors, they're just types; but what they can do is forbid code which doesn't handle errors. As for "reified types" affecting run-time behaviour, I would call those tags rather than types. For example, the class of an object is a tag, not a type.

seanmcdirmid 12y ago
> I wasn't referring to external tooling, which I agree gains a lot from strong types (specifically because a load of programs have been forbidden, which makes their job tractable). Careful. You also want to allow unsound choices in completion options, since the programmer could have made a mistake or is unaware of the more specific type needed to support some operation (especially if they are using code completion for discovery purposes). Sometimes the path between valid program A and valid program C is an invalid program B (think about editing code without the ability to create transient syntax errors...how horrible would that be!). Type theorists often get this wrong, because they are so focused on correctness :) > When dependent types and proving correctness are mentioned, there is often an assumption that some magical ability is gained. I thought magic was needed just to do the type checking. I don't think anyone who has gone through the program proving process would think it was easier (e.g. via F*), a lot of sweat is required to get those rock solid absolute guarantees. > As for "reified types" affecting run-time behaviour, I would call those tags rather than types. For example, the class of an object is a tag, not a type. This is only the overly narrow type theorist's definition of type. The class of an object is obviously a type/kind/classifier via the informal definition of type. In a statically typed language, it also happens to correspond 1-1 with the static type of the object as created, which is incredibly useful from a usability standpoint. Erasure likewise is pretty bad, and languages that don't erase (C# vs. Java) are much more usable.
tel 12y ago
Typeclasses and proof search can add expressiveness. You need not program everything but merely constrain the logic and let the compiler determine the behavior.

seanmcdirmid 12y ago

> I wasn't referring to external tooling, which I agree gains a lot from strong types (specifically because a load of programs have been forbidden, which makes their job tractable). Careful. You also want to allow unsound choices in completion options, since the programmer could have made a mistake or is unaware of the more specific type needed to support some operation (especially if they are using code completion for discovery purposes). Sometimes the path between valid program A and valid program C is an invalid program B (think about editing code without the ability to create transient syntax errors...how horrible would that be!). Type theorists often get this wrong, because they are so focused on correctness :) > When dependent types and proving correctness are mentioned, there is often an assumption that some magical ability is gained. I thought magic was needed just to do the type checking. I don't think anyone who has gone through the program proving process would think it was easier (e.g. via F*), a lot of sweat is required to get those rock solid absolute guarantees. > As for "reified types" affecting run-time behaviour, I would call those tags rather than types. For example, the class of an object is a tag, not a type. This is only the overly narrow type theorist's definition of type. The class of an object is obviously a type/kind/classifier via the informal definition of type. In a statically typed language, it also happens to correspond 1-1 with the static type of the object as created, which is incredibly useful from a usability standpoint. Erasure likewise is pretty bad, and languages that don't erase (C# vs. Java) are much more usable.

tel 12y ago

Typeclasses and proof search can add expressiveness. You need not program everything but merely constrain the logic and let the compiler determine the behavior.