2 ms·

This is quite a nice write-up, thank you. Regarding this point: >because what we'd really like is a way to specify that the type of `foo` depends on the result

This is quite a nice write-up, thank you. Regarding this point: >because what we'd really like is a way to specify that the type of `foo` depends on the result of `p?` Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. Now, "expressive" also often means "elegant" because you can express an idea easily with less verbosity in a dynamic language. A language with type inference is an interesting medium that sort of removes the expressivity of explicit type annotations while gaining the expressivity of a dynamic language in some respects.

groovy2shoes 10y ago
> Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? In the example I provided, the `bool -> (int * string) either` function is essentially a map from a `bool` to an `(int * string) either`. From a type-theoretic perspective, bool (which has two nullary type constructors, `true` and `false`) can be expressed as the sum of two units: `1 + 1` (or equivalently, `() + ()` or `unit + unit`) = `2`. If I understand your question correctly, then you're asking if we could just use some other sum type to express the branch to take, like: `type if-branch = consequent | alternative;`, and the answer is that such a type is precisely isomorphic to a Boolean -- because it consists of two nullary constructors, it can also be expressed as the sum of two units, `1 + 1` = `2`. To answer your question more directly, `p?` already is a sum type that informs `foo` which case to return: `type bool = true | false;`. > Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. "Expressive" can mean any of quite a few different things, so I wanted to be specific which I meant. In this case, I mean that untyped languages are more expressive because they're capable of expressing a greater number of programs than their typed counterparts. The ultimate goal of type theory is to eliminate that gap, but short of some miracle revelation, we've resigned to gradually filling it in. Note that this isn't the same as saying you can express it more elegantly or less verbosely in an untyped language -- there are some programs that are strictly not expressible with current type systems. That's on purpose! The point of the type system is to reject programs which have bugs caused by type errors, so we make those programs inexpressible on purpose, so it's usually a good thing to be less expressive in that way. The problem is that our type systems sometimes reject bug-free programs that actually would run totally fine simply because it wasn't able to prove that such was the case. Again, type theorists are working to improve the situation. What it comes down to is a question of what is being expressed. Taking programs as descriptions of processes, at the lowest level a language allows us to express a run-time process. Going up one level to the level of types, we can express information about the program itself. Thus, in a sense, by using a typed language we trade in the expressiveness of some processes for the expressiveness of some metaprocesses.

groovy2shoes 10y ago

> Is this situation not resolved by allowing p? to not be a bool necessarily but also a sum type that informs foo which case of a different sum type to return? In the example I provided, the `bool -> (int * string) either` function is essentially a map from a `bool` to an `(int * string) either`. From a type-theoretic perspective, bool (which has two nullary type constructors, `true` and `false`) can be expressed as the sum of two units: `1 + 1` (or equivalently, `() + ()` or `unit + unit`) = `2`. If I understand your question correctly, then you're asking if we could just use some other sum type to express the branch to take, like: `type if-branch = consequent | alternative;`, and the answer is that such a type is precisely isomorphic to a Boolean -- because it consists of two nullary constructors, it can also be expressed as the sum of two units, `1 + 1` = `2`. To answer your question more directly, `p?` already is a sum type that informs `foo` which case to return: `type bool = true | false;`. > Anyway, I like your footnote [1] which, for me, is what allows a typed program to actually be more expressive, in the sense that you can literally express the types in your head as you code, which is difficult or simply not provided in a dynamic language, despite that most developers will be "thinking in types" regardless of typing of the language. "Expressive" can mean any of quite a few different things, so I wanted to be specific which I meant. In this case, I mean that untyped languages are more expressive because they're capable of expressing a greater number of programs than their typed counterparts. The ultimate goal of type theory is to eliminate that gap, but short of some miracle revelation, we've resigned to gradually filling it in. Note that this isn't the same as saying you can express it more elegantly or less verbosely in an untyped language -- there are some programs that are strictly not expressible with current type systems. That's on purpose! The point of the type system is to reject programs which have bugs caused by type errors, so we make those programs inexpressible on purpose, so it's usually a good thing to be less expressive in that way. The problem is that our type systems sometimes reject bug-free programs that actually would run totally fine simply because it wasn't able to prove that such was the case. Again, type theorists are working to improve the situation. What it comes down to is a question of what is being expressed. Taking programs as descriptions of processes, at the lowest level a language allows us to express a run-time process. Going up one level to the level of types, we can express information about the program itself. Thus, in a sense, by using a typed language we trade in the expressiveness of some processes for the expressiveness of some metaprocesses.