From 76601aa6e734d56c0a06c4edf1e68cd313cde956 Mon Sep 17 00:00:00 2001 From: Alexander Date: Fri, 13 Jun 2025 12:56:10 -0400 Subject: [PATCH] assfrrwg --- acl.cool/site/draft/nomad.dj | 6 ++++-- acl.cool/site/writings/derive-appfun.dj | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/acl.cool/site/draft/nomad.dj b/acl.cool/site/draft/nomad.dj index 83b8e1b..9367b6e 100644 --- a/acl.cool/site/draft/nomad.dj +++ b/acl.cool/site/draft/nomad.dj @@ -18,9 +18,9 @@ end Above is a module _signature_. Signatures themselves can be thought of as relating to modules in much the same way that types relate to values (hence `module type` in the syntax): each one defines the set of all possible modules that comply with the structure it describes. In this case, we give the name "`Monad`" to the set of modules exposing _at least_ a type constructor `'a t`[^alpha], a function `return : 'a -> 'a t`, and a function `bind : ('a -> 'b t) -> 'a t -> 'b t`. Abstractly, these three items together are what constitute a monad. -It's helpful to think about what each item means in general before examining them in more concrete terms. `t` is a function from types to types, also known as a type constructor. `list` and `option` both are examples of type constructors. The presence of `t` in our `Monad` signature--- specifically the fact that it's parametric, i.e. `'a t` rather than just `t` ---represents the idea that a monad is essentially a _context_ around underlying computations of an abstract type. For some particular `'a` and some particular module that fits the `Monad` signature above, `'a` is the type of the underlying computation; that is, `t` is the generic context itself, and `'a t` is an instance of that generic context which is specific to the inner type `'a`; `'a t` is the type of alphas in the `t` sort of context. +It's helpful to think about what each item means in general before examining them in more concrete terms. `t` is a function from types to types, also known as a type constructor, or a "generic type"[^not-quite] in some languages. `list` and `option` both are examples of type constructors. The presence of `t` in our `Monad` signature--- specifically the fact that it's parametric, i.e. `'a t` rather than just `t` ---represents the idea that a monad is essentially a _context_ around underlying computations of an abstract type. For some particular `'a` and some particular module that fits the `Monad` signature above, `'a` is the type of the underlying computation; that is, `t` is the generic context itself, and `'a t` is an instance of that generic context which is specific to the inner type `'a`; `'a t` is the type of alphas in the `t` sort of context. -Hopefully, one of that multifarious bundle of phrasings made at least a little bit of sense--- what exactly is meant by "context" is the key to this whole endeavor, but I'm going to avoid addressing it directly until we're a little further along. For now, let's consider `return`. +Hopefully, something in that bundle of phrasings made at least a little bit of sense--- what exactly is meant by "context" is the key to this whole endeavor, but I'm going to avoid addressing it directly until we're a little further along. For now, let's consider `return`. If `t` is the generic context, then `return` is the function that makes it specific or "specializes" it to the type `'a` of some particular value `x : 'a`. This function takes an object[^object] of the base type `'a` and puts it into the context of `t`. The specialized context of the resulting `'a t` value will be in some sense basic, empty, default, null; it is the starting-point context that exists just to have `x` in it, so that computations involving `x` can take place in that sort of context later on. @@ -80,6 +80,8 @@ TODO: be explicit about how monads exist independently and we are _capturing_ th [^action-std]: This gives rise to a standard term. See [Monads as Computations](https://wiki.haskell.org/Monads_as_computation). +[^not-quite]: These are not exactly the same, but the similarity is more important than the difference. + So the list monad allows us to write non-determinsitic code in much the same style as we would write fundamentally simpler determinstic code (aside: this stratification is not theoretically needed, re 1ml) diff --git a/acl.cool/site/writings/derive-appfun.dj b/acl.cool/site/writings/derive-appfun.dj index f7c8074..60290f8 100644 --- a/acl.cool/site/writings/derive-appfun.dj +++ b/acl.cool/site/writings/derive-appfun.dj @@ -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. \ No newline at end of file