3 ms·

> if you doubt that, try coming up with some examples of operations you can perform on a value without knowing something about the type of that value. Interest

> if you doubt that, try coming up with some examples of operations you can perform on a value without knowing something about the type of that value. Interestingly, the fact that this reduces the domain of possible functions significantly is specifically what lends static type systems incredible power, such as described by this author who has never run his own (deployed) Haskell libraries: http://r6.ca/blog/20120708T122219Z.html http://r6.ca/blog/20120708T122219Z.html For example, the only obvious function that goes from A -> A for all possible values of A is the identity function - and I'm struggling to think of any other non-obvious function that could do the same. Of course, this only works with highly polymorphic functions, but that's still a huge statement.

Locke1689 14y ago
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.
chongli 14y ago
Keep in mind that there are (infinitely) many ways to implement the identity function. One such example (in Haskell) is: foo = head . (:[]) This is the composition of putting an element into a list with removing it from the list. You can do this with any functor.
- FreeFull 14y ago
  Which ultimately doesn't matter, because head . (:[]) doesn't behave differently from (\x -> x) no matter what the input is. The only possible variation on the id function is in how efficient it is, from fastest to never terminating.
- tmhedberg 14y ago
  > You can do this with any functor. Not to be pedantic, but being a functor has little to do with the fact that you can add and remove elements from lists. Knowing that a particular type is an instance of `Functor` tells you only one thing about that type: that you can `fmap` functions over its contents. But look at `fmap`'s type: fmap :: Functor f => (a -> b) -> f a -> f b There is no function with that type which can extract values from a functor, nor insert new ones. `fmap` can only modify the values already contained by the functor, leaving them in the container. Extraction of contained values from a wrapper and lifting/insertion of values into a wrapper require pattern matching and constructor application respectively, which means the type must have exposed constructors, a property independent of whether that type is a functor.

Locke1689 14y ago

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.

chongli 14y ago

Keep in mind that there are (infinitely) many ways to implement the identity function. One such example (in Haskell) is: foo = head . (:[]) This is the composition of putting an element into a list with removing it from the list. You can do this with any functor.

FreeFull 14y ago
Which ultimately doesn't matter, because head . (:[]) doesn't behave differently from (\x -> x) no matter what the input is. The only possible variation on the id function is in how efficient it is, from fastest to never terminating.
tmhedberg 14y ago
> You can do this with any functor. Not to be pedantic, but being a functor has little to do with the fact that you can add and remove elements from lists. Knowing that a particular type is an instance of `Functor` tells you only one thing about that type: that you can `fmap` functions over its contents. But look at `fmap`'s type: fmap :: Functor f => (a -> b) -> f a -> f b There is no function with that type which can extract values from a functor, nor insert new ones. `fmap` can only modify the values already contained by the functor, leaving them in the container. Extraction of contained values from a wrapper and lifting/insertion of values into a wrapper require pattern matching and constructor application respectively, which means the type must have exposed constructors, a property independent of whether that type is a functor.