HCoop / hcoop / debian / mlton.git / blame
| Commit | Line | Data |
|---|---|---|
| 7f918cf1 CE |
1 | FirstClassPolymorphism |
| 2 | ====================== | |
| 3 | ||
| 4 | First-class polymorphism is the ability to treat polymorphic functions | |
| 5 | just like other values: pass them as arguments, store them in data | |
| 6 | structures, etc. Although <:StandardML:Standard ML> does have | |
| 7 | polymorphic functions, it does not support first-class polymorphism. | |
| 8 | ||
| 9 | For example, the following declares and uses the polymorphic function | |
| 10 | `id`. | |
| 11 | [source,sml] | |
| 12 | ---- | |
| 13 | val id = fn x => x | |
| 14 | val _ = id 13 | |
| 15 | val _ = id "foo" | |
| 16 | ---- | |
| 17 | ||
| 18 | If SML supported first-class polymorphism, we could write the | |
| 19 | following. | |
| 20 | [source,sml] | |
| 21 | ---- | |
| 22 | fun useId id = (id 13; id "foo") | |
| 23 | ---- | |
| 24 | ||
| 25 | However, this does not type check. MLton reports the following error. | |
| 26 | ---- | |
| 27 | Error: z.sml 1.24-1.31. | |
| 28 | Function applied to incorrect argument. | |
| 29 | expects: [int] | |
| 30 | but got: [string] | |
| 31 | in: id "foo" | |
| 32 | ---- | |
| 33 | The error message arises because MLton infers from `id 13` that `id` | |
| 34 | accepts an integer argument, but that `id "foo"` is passing a string. | |
| 35 | ||
| 36 | Using explicit types sheds some light on the problem. | |
| 37 | [source,sml] | |
| 38 | ---- | |
| 39 | fun useId (id: 'a -> 'a) = (id 13; id "foo") | |
| 40 | ---- | |
| 41 | ||
| 42 | On this, MLton reports the following errors. | |
| 43 | ---- | |
| 44 | Error: z.sml 1.29-1.33. | |
| 45 | Function applied to incorrect argument. | |
| 46 | expects: ['a] | |
| 47 | but got: [int] | |
| 48 | in: id 13 | |
| 49 | Error: z.sml 1.36-1.43. | |
| 50 | Function applied to incorrect argument. | |
| 51 | expects: ['a] | |
| 52 | but got: [string] | |
| 53 | in: id "foo" | |
| 54 | ---- | |
| 55 | ||
| 56 | The errors arise because the argument `id` is _not_ polymorphic; | |
| 57 | rather, it is monomorphic, with type `'a -> 'a`. It is perfectly | |
| 58 | valid to apply `id` to a value of type `'a`, as in the following | |
| 59 | [source,sml] | |
| 60 | ---- | |
| 61 | fun useId (id: 'a -> 'a, x: 'a) = id x (* type correct *) | |
| 62 | ---- | |
| 63 | ||
| 64 | So, what is the difference between the type specification on `id` in | |
| 65 | the following two declarations? | |
| 66 | [source,sml] | |
| 67 | ---- | |
| 68 | val id: 'a -> 'a = fn x => x | |
| 69 | fun useId (id: 'a -> 'a) = (id 13; id "foo") | |
| 70 | ---- | |
| 71 | ||
| 72 | While the type specifications on `id` look identical, they mean | |
| 73 | different things. The difference can be made clearer by explicitly | |
| 74 | <:TypeVariableScope:scoping the type variables>. | |
| 75 | [source,sml] | |
| 76 | ---- | |
| 77 | val 'a id: 'a -> 'a = fn x => x | |
| 78 | fun 'a useId (id: 'a -> 'a) = (id 13; id "foo") (* type error *) | |
| 79 | ---- | |
| 80 | ||
| 81 | In `val 'a id`, the type variable scoping means that for any `'a`, | |
| 82 | `id` has type `'a -> 'a`. Hence, `id` can be applied to arguments of | |
| 83 | type `int`, `real`, etc. Similarly, in `fun 'a useId`, the scoping | |
| 84 | means that `useId` is a polymorphic function that for any `'a` takes a | |
| 85 | function of type `'a -> 'a` and does something. Thus, `useId` could | |
| 86 | be applied to a function of type `int -> int`, `real -> real`, etc. | |
| 87 | ||
| 88 | One could imagine an extension of SML that allowed scoping of type | |
| 89 | variables at places other than `fun` or `val` declarations, as in the | |
| 90 | following. | |
| 91 | ---- | |
| 92 | fun useId (id: ('a).'a -> 'a) = (id 13; id "foo") (* not SML *) | |
| 93 | ---- | |
| 94 | ||
| 95 | Such an extension would need to be thought through very carefully, as | |
| 96 | it could cause significant complications with <:TypeInference:>, | |
| 97 | possible even undecidability. |