3 ms·

Hmm? The set of functions with the type \alpha -> \alpha is trivially infinite. f(x) = x - 1 for \alpha = Z is an obvious example that's not the identity fun

Hmm? The set of functions with the type \alpha -> \alpha is trivially infinite. f(x) = x - 1 for \alpha = Z is an obvious example that's not the identity function. Or do you mean the function f(x) = x because obviously there is only one such function (and it's called the identity function).

tikhonj 14y ago
I think he meant the type ∀α. α → α. At least in Haskell, there is only one non-⊥ function of this type: id. Moreover, there is no non-⊥ value of the type ∀α. α. There is a tool called Djinn which can actually provide functions of such sufficiently constrained types. Another example would be the type ∀α.∀β. (α, β) → α, which only contains fst. Even types that contain an infinite number of functions can have interesting constraints from polymorphism like this. For example, the type ∀α. [α] → [α] contains a whole bunch (for sufficiently infinite values of "whole bunch" :P) of different functions. However, you are guaranteed that the functions can only affect the structure of the list: the function cannot create or modify values of type α in the list. So the function reverse would have this type, but a function which added 1 to each element of the list could not. Moreover, a function of this type would always have to map [] to [].
derleth 14y ago
> f(x) = x - 1 for \alpha = Z What? The whole point of what you're replying to is that \alpha remains undefined. Once you specify \alpha, of course you can specify more interesting functions. IOW, write a function that works even if \alpha is a composite datatype the details of which I refuse to disclose.
- Locke1689 14y ago
  ah, he didn't existentially qualify the type
  - TeMPOraL 14y ago
    That was his whole point. For all possible values and types of A, the only trivial function he found that goes A -> A is identity function.

tikhonj 14y ago

I think he meant the type ∀α. α → α. At least in Haskell, there is only one non-⊥ function of this type: id. Moreover, there is no non-⊥ value of the type ∀α. α. There is a tool called Djinn which can actually provide functions of such sufficiently constrained types. Another example would be the type ∀α.∀β. (α, β) → α, which only contains fst. Even types that contain an infinite number of functions can have interesting constraints from polymorphism like this. For example, the type ∀α. [α] → [α] contains a whole bunch (for sufficiently infinite values of "whole bunch" :P) of different functions. However, you are guaranteed that the functions can only affect the structure of the list: the function cannot create or modify values of type α in the list. So the function reverse would have this type, but a function which added 1 to each element of the list could not. Moreover, a function of this type would always have to map [] to [].

derleth 14y ago

> f(x) = x - 1 for \alpha = Z What? The whole point of what you're replying to is that \alpha remains undefined. Once you specify \alpha, of course you can specify more interesting functions. IOW, write a function that works even if \alpha is a composite datatype the details of which I refuse to disclose.

Locke1689 14y ago
ah, he didn't existentially qualify the type
- TeMPOraL 14y ago
  That was his whole point. For all possible values and types of A, the only trivial function he found that goes A -> A is identity function.