Something @jaror said in another thread got me thinking while working on an update (soon! I swear!) to the compiler, that I felt was worth posting about
I would like to expand on this, as it is relevant to my current work in making Haskell homomorphic - I have had to ‘de-magic’ IO, which means understanding both what it actually is trying to do, and how it is achieving it. Until I build a lifted type, everything is unlifted!
But there’s a twist - in my machine, there is both a yard (cons cells, immutable tape with linear access) and a heap (structs, potentially mutable memory with random access), so a lifted type could live in either. This is part of how I’m making Haskell homomorphic - the yard will eventually be allocated inside of the heap, along side the machine descriptor, and with a large enough yard and agressive garbage collection, we can simulate heap, closing one of the necessary loops. Every yard address is a heap address is a host address.
Unlifted types have something that lifted types don’t (or, have less of). They have ‘placement’. This is related to ‘linguistic displacement’, but also ‘displacement’ as in distributed computing, and also I have a suspicion that I have accidentally re-invented modal type systems, if my cursory investigation into them is correct.
All of this is very important, because one of the goals of this compiler isn’t just to better describe how Haskell works at the low-level (eg, my work on memory), but also to better describe how one computers work at the network level - I got into Haskell to build self-organizing distributed networks before I fell ill, and I always intended to return to that.
Big aside: What is placement, a rough sketch
Placement is the meta-information of ‘who what where when why and how’ - or, if you will, it is the contents of the pointer represented by the RealWorld token in GHC. It is the context in which a computation runs - or, rather, having a computation having placement creates a set of adjoint / forgetful functors* differing by their placement.
* I hope I have this terminology correct enough
It is important to understand some concepts:
- Low-level is describing how one computer is made up of many smaller computers.
- A network describes how one computer is made up of many smaller computers
- Both are placement
- Placement isn’t a kind (shape), not really
- Things can have a kind, and a place
- We can describe placement using types, but its always a local type, because placement is what gives types and data a place to live / be stored / executed.
- Placement means
"foo" :: Your Stringis a different type than"foo" :: My String, but my Your can be your My and vice versa, which is part of why placement isn’t just a kind - This is one of the reasons that using just a type system to describe memory has been difficult - something was missing
- Its concerned with how the same concept may have many different implementations - such as IO vs effect systems
- Placement concerns both the machine that is (usually) way-below, and the network that is (usually) way-above
- It is also how you describe the ambiguity of incomplete information aka ‘knowability’ itself.
- Way-above and way-velow are part of lattice theory and have special meaning, but in this context essentially are the addition of ‘dont-know’ and ‘dont-care’ to the usual boolean true and false - one of the reasons that I am adamant that we need a proper Boolean class, for things like this 4-logic
Here are some pretty image I made a long time ago:
Their similarity to Penrose diagrams is not accidental, Penrose diagrams are just the special case for physical spacetime. I use it to describe causal placement in distributed computing, to describe not just what a computer knows, but also what it doesn’t know, can’t know, doesn’t care to know, and what it has forgotten.
This is pertinent in describing how type information gets thrown away, or how the runtime manages the memory lifecycle, only it can be applied inwards (the machine) or outwards (the network)
Notably, placement is also what gives grammars the uniquely-human feature of linguistic ‘tenses’, which allow us to refer to or infer (analogous to type inference!) the context in which things are placed, displaced from, or replaced in. Specifically, placement inference allows us to say “Fred threw his ball at me”, instead of complex sentences such as “there exists a past moment in which the entity indicated by the name Fred used a hand-part to grip and throw a ball with a trajectory impacting the entity indicated by the name Leo in a future moment”
Back to Stripping the Magic from the RealWorld
Anyway, since I am making Haskell homoiconic, I actually have to make it not magic. This means understanding exactly what IO and RealWorld actually are, what they are doing, and why they are doing it.
IO is defined as:
newtype IO a = IO (State# RealWorld -> (# State# RealWorld, a #))
The hashes on the parenthesis (# #) are just fluff to indicated unboxed primitives - unboxed meaning that they are still in CPU registers or on the immediate stack that’s guaranteed to stay in-cache. GHC uses this to guarantee that they get used immediately, forcing strict behavior, but LHC is strict and unlifted by default so they are sort of implied, leaving us with a simple state monad over State# RealWorld - see for comparison:
newtype IO a = IO (State# RealWorld -> (State# RealWorld, a)
newtype ST world a = ST (State# world -> (State# world, a)
newtype State st a = State (st -> (st, a))
The hash on the State# type actually has no special meaning itself, and is only used to indicate that it is a primitive type.
What is special, is a combination of two things:
- Simply by threading state through a sequence of computations, it forces them to occur in sequence - this is purely a consequence of IO being a subset of the State monad, and has nothing to do with
State# RealWorld - The
State# worldtype itself is a type with zero size, and so the state argument gets erased as a completely separate optimization, which happens later
Together, they give us a way of enforcing computations to happen in sequence, with zero-runtime-overhead!
data State# s :: ZeroBitType -- Erased by the compiler
data RealWorld -- Not a zero bit type, actually a ptrarg! Its primitive, but its lifted!
Thus, when State# st or State# RealWorld getserased , ST st / IO just becomes identity:
newtype ST wo a = ST a
newtype IO a = IO a
What’s interesting is that RealWorld is actually a ptrArg, meaning despite having non constructors, it has a size. This is why its deeply magical.
In a homoiconic haskell, it isn’t magical. It is actually a real pointer, to the machine self-reference in its own heap. We can still pull the same trick to elide the argument for efficiency, but we’ve closed another self-reference loop.
So, RealWorld represents the placement of the currently executing script - you could describe succincntly as ‘HereNow’ - and we can actually talk about running a VM inside of a VM, and using the inner RealWorld to call the super-RealWorld of the host VM, allowing us to naturally implement things like sandboxed environments.
Type towers
I am now going to make the argument that the IO monad being a state monad over ‘the real world’ isn’t an accident or happenstance, it is a consequence of extending the standard type system of sums products and exponents, to include tetration.
In mathematics, some properties require a sufficient number of operands.
- the properties of the boolean complement only requires one operand:
x == !(!x) - the properties of commutativity require two
(x + y) == (y + x) - the properties of associativity require three
(x + y) + z == x + (y + z)
This increase in the number of dimensions is a consequence of the Cayley Dickson construction see also Clifford algebras - note that things become pathologically strict at higher dimensions and start repeating themselvese (power sets) or crashing (non-trivial zero divisors), in ways roughly analogous to adjoint / forgetful functors and bottom.
The sum / product / exponent type system is the same - it requires new ‘operands’ to grow beyond a certain dimension - or, type parameters in our case.
Let explore what that means - I’m going to continue by extending this comment but we’ll start at the beginning and craft our power tower up from scratch.
We start with the zero-arity fixed point recursion, called Lang here
-- Zero-arity (the f is recurse, it points to itself, and is not the 0th argument)
newtype Lang f = Lang (f (Lang f))
It’s the only zero-arity operator, because its the thing that gets the arities applied to it.
Did you know that you can / must use recursion to define Nil?
Given
data Cons a r = Cons a ryou must eitherdefinenil = Cons nil nilor else define a new, separate Nil value, or else you must use some other value as nil and make that value unrepresentable. This is a neat consequence of Lists[]vs Tuples()and explains why the zero-tuple()isn’t real (real Nil is always[]) and explains why nor is the single tuple(a)- its just(a, Nil)and that’sa:Nilaka[a]. For safety, my implementation uses a special NIL_ADDR pointing to a recursive nil cons cell to support both.
Unary functors are predictable. Void, Proxy (Nil), and Identity (Atom) functors
-- Single arity
data Void a r -- V1 a, Const Void a, Empty a
data Nil a r = Nil -- Proxy a
data Atom a r = Atom a -- Const a r (sic)
Now come the binary sum and product functors:
-- Functor.Sum / Coproduct
data Sum f g a = InL (f a) | InR (g a)
deriving (Functor)
infixr 6 :+
type (f :+ g) = Sum f g
-- Functor.Prod / Product
data Prod f g a = Prod (f a) (g a)
deriving (Functor)
infixr 7 :*
type (f :* g) = Prod f g
-- Now we can do this:
-- type LambdaCalculus = Var :+ Lam :+ App
Just for fun, we’ll add free and cofree:
infixr 6 :|
type Free f a r = a :+ f r
type (:|) f a r = Free f a r -- Oh god I hate operators but in this case, justified
-- type DistributedJson = Lang (Json :| URL) -- A json file where some nodes are replaced with URLs to download the rest from
infixr 7 :&
type Cofree f a r = a :* f r
type (:&) f a r = Cofree f a r -- Ditto
-- typed AnnotatedAST = Lang (Lambda :& SrcPos) -- An AST annotated with source positions
Our last binary functor type
-- Functor.Exp / Exponent types (functions)
data Exp f g a = Exp (f a -> g a)
infixr 8 :^
type (f :^ g) = Exp f g
-- We almost always just use `->` but it can be other arrows too like linear arrows and stuff.
This is usually where the power-tower of types stops. It stops at exponent types - aka functions, parameterizing type over itself in the sense that for every input there is an output. This uses up all of our inputs, so nothing we do now, is new.
This is kind of like saturating the dimensions - we have sums, which allow us to have one type or another in the same place, products which allow us to have one type and another in the same place at the same time, and exponents that take us from one type to another allowing a value to be of one type at one time and another type later, and this completes all possible interactions at this level.
Tet
Well, not all possible interactions. We could be sending a program from one context, to another
Tetration types parameterize computation over where they occur - so even though functions may have the same inputs and outputs and even the same source code, they are functionally different functions, running on different machines, possibly with different architectures.
Tetration expresses placement or implementation or the intended run-space such as ‘here, now, on this computer’. Tetration captures such things as the local computer and what architecture its running on (eg Haskell AMD64 vs Haskell X86). It also captures the concept of sending a program to another computer / context.
Back to placement, here’s what we know:
- Placement is modal type theory or something close - it includes spatial and temporal logic but also more
- Two otherwise identical functions are still different if they run in different worlds
- Portable / mobile code needs to know where its going to run
- If an exponent type is
a -> b, then a… placement isPlace (a -> b)? - Ie, where
Place a = World -> (World, a), which is justIOandRealWorld - Its parameterized by the location / world / evaluation context it is running in
- So World is
State# RealWorldin GHC, and because GHC is ignorant of Tet, it all runs ‘here-now’ - More specifically,
State#is tet, RealWorld is just a tag - which local context - More specifically, RealWorld is a ‘ptrarg’ (eg, a heap addr) that COULD point
to the machine context, but just gets erased - We can actually make it point somewhere, allow it to be erased, and still
find a way to provide magic access to it, to allow eg access to file handles
and such - GHC documentation for RealWorld
- it says: “RealWorld is deeply magical. It is primitive, but it is not
unlifted (hence ptrArg). We never manipulate values of type RealWorld;
it’s only used in the type system, to parameterise State#.”
- it says: “RealWorld is deeply magical. It is primitive, but it is not
- primitive means "built-in that the runtime is dependent on’
- lifted means ‘its a regular haskell value, it could be a value or a thunk or
undefined or bottom but its memory and lifecycle is managed by the runtime’`1- eg just a pointer to a managed heap object
- ptrarg means that its type is actually a ptr / makes the compiler treat it as
lifted even though its magic - RealWorld theoretically a wrapper around a pointer some representation of the
machine’s context, allowing it to be referenced as a singleton type, which
would otherwise need to be hardcoded as an address or special function or
passed as an implicit param or something - State# forces it to be zero-sized and thus elidable
- We can actually reference to the machine context’s position in its own heap
while allowing State# to elide it - We can have more than one type of RealWorld - realworld might be Machine, or
it might be VM Machine, or VM (VM Machine), etc - its the actual sandbox
itself or the supervisor or owning program or whatever - a script can reference what its running in
- getting the actual machine pointer is magical like unsafePerformIO
- Place(ment) is more than just IO
- it generalizes it to be ‘the sum of all effects available on this machine’
- it doesn’t have to be an effect system, but it can be expressed as one
- it also allows expressing of cryptographic concepts such as private and public data
The question is, how do we expose this as syntax? Well, the answer is already staring at us. We use monads and monad transformers.
In the end, I ended up with this:
-- Functor.Tet / Tetration types aka 'height' or 'placement'
-- The mathematical name for the tetration operands are 'base' and 'height'
-- This is extremely appropriate, given that we are working with 'base' functors
-- and 'height' is itself a colloquial placement (think altitude)
-- We saturated the binary types so we have a new `h` argument
data Tet f g h a = Tet (h (f a -> g a))
-- NOTE: Tet appears to generalize monad and arrow transformers
infixr 9 :@
type (:@) f h a = Tet f f h -- Winner! Because its full transformers that need g
-- Eg, `Lang (Foo :@ IO) = IO (Lang Foo -> Lang Foo)
-- An arrow with effects; it takes us from the lang, to itself, hence Tet f f h
-- At last, syntax for placement! Examples:
-- Combinator calculus with IO: Lang ((Var :+ App) :@ IO)
-- Haskell with remote invocation: Lang (Haskell :@ Remote IO https://foo.com)
-- An effect system: Lang (Haskell :@ Eff '[ Read, Write, Foo ])
Its just monad syntax! What!
It turns out we have been using monads and monad transformers and effect systems as a poor man’s tetration type this entire time.
I actually put off designing exactly how I was going to handle this, but the research has lead here, even though I deliberately kept myself open to other alternatives. All roads really do lead to Ankh Morpork monads.
Given that this is functor types, eg functor sum, functor product, functor exponent, it makes sense that we are talking about functor tetration, eg parametrizing all functors with worlds, and that’s just monad syntax. It is slightly important to note that h :: place is not necessarily a monad, eg in data Tet f g h a = Tet (h (f a -> g a)) - it could be eg arrow or something lesser.
So, with this definition, using Tetration types, we can talk about placement, which also includes memory management, eg allowing us to describe the difference between type Lifted = Lang ((Haskell :+ Bottom) :@ Heap) and type Unlifted = Lang (Haskell :@ Yard) thus removing even more magic.
Even more pleasing, I didn’t have to add a Machine self-reference register or opcode to do it, like I was thinking of doing - that would have been too much magic. Now, I can directly access the machine context and the top-level environment, way more efficiently than traversing upwards from the bottom.
Don’t forget, Tet types also allow you to parametrize arrow types because they are higher up than Exponents like (->), and so you can use Tet to differentiate different evaluation models, which, obviously, duh! That was the point!
Anyway, these notes were starting to fill up my compiler implementation, and I needed to get them out and put them somewhere so they live here now.
So keep pointing these things out.
Its always useful to study how other domains have different ways of describing the same thing - each new way of implementing a structure has the potential to reveal a new facet to our understanding of the structure.
Another relevant example is all of the different ways of implementing / understanding free monads (free, church encoded, free-er, codensity) and effect systems (not even going to bother listing).