# Paper Reading: Lightweight-Higher-Kinded-Polymorphism¶

PDF is available online.

## How-To¶

In fact, the technique (hereafter as **LHKP** ) introduced in this paper works perfectly only when
the order of types is less than 2 (have kind `*`

or `* -> *`

) and type
constructor is not an endofunctor.

LHKP achieves first order types through a parametric interface type `type ('a, 't) app`

, denoted as
`'a 't`

in higher kinded ML, where `'a`

is applicated to `'t`

where `'t`

has kind
`* -> *`

.

```
type ('a, 't) app
module type App = sig
type 'a s
type t
external inj : 'a s -> ('a, t) app = "%identity"
external prj: ('a, t) app -> 'a s = "%identity"
end
```

For any problem with `%identity`

,
check %identity in OCaml.

We can then make intuitive explanations using the implementation of polymorphic `map`

.

```
val map: forall t a b {t <: mappable} .(a -> b) -> t a -> t a
```

Firstly, present the common part for all type constructors/applications (`App`

) here:

```
module Common = struct
type t
external inj : 'a -> 'b = "%identity"
external prj : 'a -> 'b = "%identity"
end
```

Then declare a *type class* :

```
module type Mappable = sig
type t
val map: ('a -> 'b) -> ('a, t) app -> ('b, t) app
end
type 'a mappable_impl = (module Mappable with type t = 'a)
```

Interesting, we’ve just implemented a type class tersely just like in Haskell.

Next, let’s implement the `list`

type constructor:

```
module ListApp : App with type 'a s = 'a list = struct
type 'a s = 'a list
include Common
end
```

Now we’ve almost achieved the final goal, and what’s left to do is still similar to Haskell for
we’re exactly going to implement type class `Mappable`

for type constructor `list`

:

```
module MapList : Mappable with type t = ListApp.t = struct
type t = ListApp.t
let map (f: 'a -> 'b) (ca: ('a, t) app): ('b, t) app =
let ca = ListApp.prj ca
in let cb = List.map f ca
in ListApp.inj cb
end
```

And finally, we got a polymorphic `map`

:

```
let map (type t) (m: t mappable_impl) (f: 'a -> 'b) (a: ('a, t) app) =
let module M = (val m : Mappable with type t = t)
in M.map f a
let () =
let lst = ListApp.prj(map (module MapList) (fun x -> x + 1) (ListApp.inj [1; 2; 3]))
in List.iter print_int lst
```

We can also use the same `map`

to work with `Array`

type constructor:

```
module ArrayApp : App with type 'a s = 'a array = struct
type 'a s = 'a array
include Common
end
module MapArray : Mappable with type t = ArrayApp.t = struct
type t = ArrayApp.t
let map (f: 'a -> 'b) (ca: ('a, t) app): ('b, t) app =
let ca = ArrayApp.prj ca
in let cb = Array.map f ca
in ArrayApp.inj cb
end
```

Now, we can show our polymorphic functions:

```
let lst_data = [1; 2; 3]
let arr_data = [|1; 2; 3|]
let lst_data_hkt = ListApp.inj lst_data
let arr_data_hkt = ArrayApp.inj arr_data
let lst_mapped : (int, ListApp.t) app = map (module MapList) (fun x -> x + 1) lst_data_hkt
let arr_mapped : (int, ArrayApp.t) app = map (module MapArray) (fun x -> x + 1) arr_data_hkt
let () = List.iter print_int (ListApp.prj lst_mapped); print_string "\n"
let () = Array.iter print_int (ArrayApp.prj arr_mapped); print_string "\n"
```

That’s all about the core secrets of implementing type classes and HKT with this approach.

## Static Resolution: More polymorphic¶

Take care that, in last section, the so-called **LHKP** is also kind of disgusting because we have to give the type constructor manually.

```
map (module MapList) ...
map (module MapArray) ...
```

It’s obvious that, type constructors like `MapList`

and `MapArray`

had already been
given in other arguments:

```
val map: type t. (t mappable_impl) ('a -> 'b) -> ('a, t) app -> ('b, t) app
```

In fact, the argument typed `t mappable_impl`

is unique given a unique `t`

(in other words, `mappable_impl`

is injective).
So how about create an instance of type `t mappable_impl`

automatically from the type `t`

?

If we can do this, we then have a better polymorphism no worse than Haskell’s.

```
val arr_data: ('a, ArrayApp.t) app
val lst_data: ('a, ListApp.t) app
val f: 'a -> 'b
map f lst_data: ('b, ListApp.t) app
map f arr_data: ('b, ArrayApp.t) app
```

Yes, that’s possible, actually we could use type variable inside a generic function/value to instantiate the type constructor.

Another obscure thing is that, type variable deciding the instantiation of type constructor might not appear in parameters, return type can also be used to do such things.

This kind of instantiation could be implemented through the static resolution/static duck typing, which is provided by F# language, empowering us to use almost full-featured type classes and higher kinded types.

This technique would be introduced in this article: 更高更妙的F#.

For OCaml alternatives, check modular implicits .

## Limitation1: Much Higher Kinded¶

When it comes much higher kinded types(like `* -> * -> *`

),
in haskell it’s notable trivial:

```
data Either a b = Left a | Right b
```

However, in many polupar ML languages like OCaml and F#, we have to use

```
type ('a, 'b) either = Left of 'a | Right of 'b
module EitherApp (Q: sig type t end): App with type 'a s = (Q.t, 'a) either = struct
type 'a s = (Q.t, 'a) either
include Common
end
```

Then `Either Int`

in haskell can be written in OCaml as

```
module IntModule = struct
type t = int
end
module EitherInt = EitherApp(IntModule)
```

Let’s implement `Functor`

class for `forall a. Either a`

:

```
module MapEither (Q: sig type t end): Mappable with type t = EitherApp(Q).t = struct
module EitherApp2 = EitherApp(Q)
type t = EitherApp2.t
let map (f: 'a -> 'b) (ca: ('a, t) app) : ('b, t) app =
let ca = EitherApp2.prj ca
in let cb =
match ca with
| Left l -> Left l
| Right r -> Right (f r)
in EitherApp2.inj cb
end
```

However, using such `Either`

could be quite annoying:

```
let either_data1_hkt =
let module M = EitherApp(IntModule) in M.inj (Left 1)
let either_data2_hkt =
let module M = EitherApp(IntModule) in M.inj (Right 2)
let either_map e =
let module Data = EitherApp(IntModule)
in let module Map = MapEither(IntModule)
in let res = map (module Map) (fun x -> x + 1) e
in Data.prj res
let either_mapped1 = either_map either_data1_hkt
let either_mapped2 = either_map either_data2_hkt
let show_either_int_int e =
match e with
| Left l -> "Left " ^ string_of_int l
| Right r -> "Right " ^ string_of_int r
let () = print_string (show_either_int_int either_mapped1 ^ "\n")
let () = print_string (show_either_int_int either_mapped2 ^ "\n")
```

That sucks so much for the lack of modular implicits and, it’s an internal property that
expressing much higher kinded types (whose kind ascription is more complex than `* -> *`

)
requires many other boilerplate codes like `('c, ('b, 'a) app) app`

.

## Limitation2: Identity¶

The second problem could be a little sensitive in the senarios where identity type constructor is in need.

A vivid example is `MonadTrans`

, for the consistency between `StateT`

and `State`

.

```
newtype StateT s m a = StateT { runStateT :: s -> m (a, s) }
type State s a = StateT s Identity a
type Identity a = a
```

The problem occurs at `s -> m (a, s)`

, when `m = Identity`

, `m (a, s) = (a, s)`

.

More concretely, in OCaml, `('a * 's, identity) app`

cannot become `'a * 's`

directly, which means that
an extra `prj`

is required here.

Then the implementation of `State s a`

cannot be equivalent to
Haskell, for we have to manually perform `prj`

each time after invoking `runState/runStateT`

.

## Why this Lightweight-Higher-Polymorphism instead of the Haskell approach¶

According to the authors’ arguments, an awkward scene in OCaml is, type aliases and actual type signatures cannot be distinguished from each other, which makes it impossible to directly perform unification after introducing higher kined types.

```
'a cons ~ 'e 't
```

Now we don’t know if `cons`

is a type constructor or simply an alias,
so we cannot say `'a ~ 'e`

and `cons ~ 't`

, in case `'cons`

is a type alias like

```
type 'a cons = ('a * 'a) list
```

where `'a cons ~ 'e 't`

should imply `('a, 'a) ~ 'e`

and
`list ~ 't`

.

So why not process type aliases firstly and convert them into regular types containing no aliases? The paper said “Since OCaml cannot distinguish between data types and aliases…”, I think it’s not true, for OCaml types are named with lowercase leading character, while datatype constructor are given through names that start with uppercase character.

```
type <datatype> = | A of type
type 'a <alias1> = 'a list
type <alias2> = int
```