# Tetration types: Making IO and RealWorld without Magic

**URL:** <https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802>\
**Category:** Uncategorized\
**Created:** [October 5, 2026, 10:30pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802 "2026-10-05T22:30:32Z")\
**Posts on this page:** 8\
**Page:** 1

<div class="post-metadata">

**Author:** ![ApothecaLabs](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/apothecalabs/32/3215_2.png) [@ApothecaLabs](https://discourse.haskell.org/u/ApothecaLabs)\
**Post date:** [October 5, 2026, 10:30pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/1 "2026-10-05T22:30:32Z")

</div>

Something @jaror [said in another thread](https://discourse.haskell.org/t/you-dont-need-an-effect-system/14792/5) got me thinking while working on an update (soon! I swear!) to [the compiler](https://discourse.haskell.org/t/announcing-little-haskell-compiler-v0-1-0-pre-release-try-it-online/14702), that I felt was worth posting about

> [@You don't need an effect system](https://discourse.haskell.org/t/you-dont-need-an-effect-system/14792/5):
>
> Unlifted types have little to do with the allocation itself, more with the memory layout and when evaluation happens

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 String` is 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:

 ![one-two-many](https://us1.discourse-cdn.com/flex002/uploads/haskell/original/2X/d/de8e950af11ed7f6b2540bda2f5b084f65dc6f5c.png)  
 ![Way-below-time](https://us1.discourse-cdn.com/flex002/uploads/haskell/original/2X/c/cd84ddb9e112269cfa5eebb98b3dcee599331566.png)

Their similarity to [Penrose diagrams](https://en.wikipedia.org/wiki/Penrose_diagram) 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:

```haskell
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:

```haskell
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# world` type 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!

```haskell
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:

```haskell
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](https://en.wikipedia.org/wiki/Cayley%E2%80%93Dickson_construction) - 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](https://discourse.haskell.org/t/announcing-little-haskell-compiler-v0-1-0-pre-release-try-it-online/14702/22) 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

```haskell
-- 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 r` you must eitherdefine `nil = Cons nil nil` or 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’s `a:Nil` aka `[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

```haskell
-- 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:

```haskell
-- 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:

```haskell
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

```haskell
-- 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 is `Place (a -> b)`?
- Ie, where `Place a = World -> (World, a)`, which is just `IO` and `RealWorld`
- Its parameterized by the location / world / evaluation context it is running in
- So World is `State# RealWorld` in 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](https://hackage-content.haskell.org/package/base-4.22.0.0/docs/GHC-Base.html#t: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#.”

- 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:

```haskell
-- 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.

---

<div class="post-metadata">

**Author:** ![olf](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/olf/32/3813_2.png) [@olf](https://discourse.haskell.org/u/olf)\
**Post date:** [October 6, 2026, 8:15pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/2 "2026-10-06T20:15:54Z")

</div>

> [@ApothecaLabs](#):
>
> ```haskell
> data Exp f g a = Exp (f a -> g a)
> deriving (Functor)
> 
> ```

```haskell
error: [GHC-16437]
    • Can't make a derived instance of ‘Functor (Exp f g)’:
        Constructor ‘Exp’ must not use the type variable in a function argument
    • In the data declaration for ‘Exp’

```

---

<div class="post-metadata">

**Author:** ![mixphix](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/mixphix/32/5629_2.png) [@mixphix](https://discourse.haskell.org/u/mixphix)\
**Post date:** [October 6, 2026, 8:18pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/3 "2026-10-06T20:18:18Z")

</div>

Also, wouldn’t `f :^ g` usually mean `g a -> f a`, considering `(2 ^ 3) ~ (3 -> 2)`?

---

<div class="post-metadata">

**Author:** ![ApothecaLabs](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/apothecalabs/32/3215_2.png) [@ApothecaLabs](https://discourse.haskell.org/u/ApothecaLabs)\
**Post date:** [October 6, 2026, 8:55pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/4 "2026-10-06T20:55:54Z")

</div>

@olf

Woops! Yes, I had to remove that. Can’t have the elements in the left hand side and still derive functor!

Also `:@` was improperly defined too - I had to sleep on it before I remembered that `Tet` is by default a transformer, so `type (:@) f h a = Tet f f h a` which is finally how I get my `Lang (Haskell :@ IO)` syntax.

This really is more notes using Haskell syntax, than intended-to-be-compileable code, mostly because GHC really hates some of the things I’m doing, even if its logically sound - it really hated when I tried to `type f g a :@ h` earlier.

I do gradually beat the compiler / type system into submission though 🤣 So keep pointing these things out.

* * *

@mixphix  
I think you might be right!

Exponentiation is where things split / becomes non-commutative, and you suddenly have handedness and two inverses! I was mirroring usage syntax, base ^ exponent, but mathematically speaking, its the exponent that is paremeterized by the base, so, as you say, it should be:

```haskell
data Exp f g a = Exp g a -> f a

```

But the infix operator should still be:

```haskell
infixr 8 :^
type f :^ g = Exp f g

```

Keeping our usage as `base ^ exp`

* * *

I have also fixed the definition of `:@`:

```haskell
infixr 9 :@
type (:@) f h a = Tet f f h
-- Lang (Foo :@ IO) = IO (Lang Foo -> Lang Foo)

```

I had to realize that if it generalizes monad and arrow transformers, it needs to be endo / f needs to be sent to itself, to represent plain / non-transformer monads and arrows. But now I get my lovely placement syntax for things like `Lang ((Var :+ App) :@ IO)` and `Lang (Haskell :@ Eff '[Read, Write, Foo])`

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [October 6, 2026, 10:22pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/5 "2026-10-06T22:22:40Z")

</div>

Actually, exponentiation can be defined using the Yoneda embedding:

```haskell
data Exp f g a = Exp (forall b. (a -> b) -> g b -> f b)

instance (Functor f, Functor g) => Functor (Exp f g) where
  fmap f (Exp h) = Exp (\g -> h (g . f))

```

This is the standard way of defining exponential objects in the category of presheaves (`Exp f g` is an object in PSh(Set) if you pretend Hask is the same as Set).

To make it a bit more obvious:

```haskell
data Morphism f g = Morph (forall x. f x -> g x)
data Yo a x = MkYo (a -> x) 
data Product f g x = MkProduct (f x) (g x)

data Exp f g x = Exp (Morphism (Product (Yo x) g) f)

```

Note that you should think of `Yo`, `Product`, and `Exp` as partially applied (without the `x` argument) yielding endofunctors on Hask. Morphisms are just sets (approximated by `Type`) and not objects, so they don’t need to be partially applied.

---

<div class="post-metadata">

**Author:** ![ApothecaLabs](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/apothecalabs/32/3215_2.png) [@ApothecaLabs](https://discourse.haskell.org/u/ApothecaLabs)\
**Post date:** [October 6, 2026, 10:54pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/6 "2026-10-06T22:54:55Z")

</div>

Sheafification is a bit outside my usual studies, but I’ve run into it enough to know that (pre)sheaves are definitely an adjacent / formal / one way of talking about some of the things I study, so I ought to spend more time on it - and alternative perspectives and definitions of things are often so good at revealing deep connections.

I’m going to be pondering this tonight 🙂

---

<div class="post-metadata">

**Author:** ![jaror](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/jaror/32/3271_2.png) [@jaror](https://discourse.haskell.org/u/jaror)\
**Post date:** [October 7, 2026, 12:39pm UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/7 "2026-10-07T12:39:58Z")

</div>

Don’t worry too much about the presheaves. I only really mentioned those because I’ve been working with those a lot recently. It is probably better to just think about the category of endofunctors on Hask.

---

<div class="post-metadata">

**Author:** ![ApothecaLabs](https://sea2.discourse-cdn.com/flex002/user_avatar/discourse.haskell.org/apothecalabs/32/3215_2.png) [@ApothecaLabs](https://discourse.haskell.org/u/ApothecaLabs)\
**Post date:** [October 8, 2026, 1:59am UTC](https://discourse.haskell.org/t/tetration-types-making-io-and-realworld-without-magic/14802/8 "2026-10-08T01:59:30Z")

</div>

Oh yeah, its like fiber bundles in geometric algebra 😆 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.

Your example of an provided implementation of `Exp` is a wonderful example of such 🥰 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).

(It is also quite reassuring to have other domains as a sanity check, too! And even if I do prefer my own understanding as cast through the lens of ‘placement’, I do like being able to talk to other people about my ideas in their own domain language, where they are far more likely to understand me)