This commit is contained in:
Alexander 2025-06-13 12:56:10 -04:00
parent dce20ad6fc
commit 76601aa6e7
2 changed files with 5 additions and 3 deletions

View file

@ -45,6 +45,6 @@ It turns out that there are multiple ways to implement the derivation functors--
The modules above that seem to have parameters, do; these modules are called "functors". A functor in OCaml parlance is distinct from anything called a "functor" elsewhere, being essentially a function from modules to modules. For practical reasons, modules and value-level programs are stratified from one another in OCaml, so a functor does not literally have a function type, but the mental model is still basically correct.
A subtlety of the OCaml module system is that if a module is defined with a particular `module type` a.k.a. signature attached, e.g. `module M : S = struct...`, all the types that are abstract in the signature `S` will _also_ be abstract in the module itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal. This is because both types are abstract, meaning the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above, `Functor with type 'a t = 'a M.t`--- for example ---exposes the equality of the two types, so that functions defined as expecting arguments of `'a t` can accepts `'a M.t`, and _vice versa_.
A subtlety of the OCaml module system is that if a module is defined with a particular `module type` a.k.a. signature attached, e.g. `module M : S = struct...`, all the types that are abstract in the signature `S` will _also_ be abstract in the module itself. This means that the compiler can't see or be convinced that for some `F (M)` with `type t = M.t` in `F`, `M.t` and `(F (M)).t` are equal. This is because both types are abstract, meaning the underlying type is not available. To fix this, we can explicitly expose the equality by using the `with type` construct. In the above, `Functor with type 'a t = 'a M.t`--- for example ---exposes the equality of the two types, so that functions defined as expecting arguments of `'a t` can accept `'a M.t`, and _vice versa_.
[^falsehood]: Unsurprisingly, that's a lie. You have to buy a `Monad` first.