haskellmonadsfixpoint-combinators# What's the intuition behind fixpoints of monads NOT being the direct limit?

Consider the following datatype:

```
data Foo = Halt | Iter Foo
```

This is the fixpoint of `Maybe`

. It *contains* the direct limit of the sequence `Void`

, `Maybe Void`

, `Maybe (Maybe Void)`

and so on, where `pure`

is the injecting morphism. However, `Foo`

has an element *not* covered by the direct limit, namely `fix Iter`

.

Let me have another example:

```
data Bar = Bar Bar Bar
```

This is the fixpoint of `Complex`

. Since `Void`

, `Complex Void`

, `Complex (Complex Void)`

and so on are all homeomorphic to `Void`

, the direct limit is also `Void`

. However, `Bar`

has an element, namely `fix (join Bar)`

.

So what's the mathematical justification of those "leftover" elements?

Solution

As was pointed out in the comments, these elements exist as a consequence of nontermination.

In a terminating language, or equivalently, in the category of sets, the initial algebra (least fixed point) of `Maybe`

is `Nat`

and the initial algebra of `Complex`

(`data Complex a = Complex a a`

) is the empty type `Void`

. `fix Iter`

and `fix (join Complex)`

don't exist because `fix`

is not definable in a terminating language.

With unrestricted nontermination, sets are no longer a good model of types because the infinite loop inhabits all types. A common alternative in that case are DCPOs or some similar order structure. In particular, the existence of bottom and of limits for increasing sequences are just what is needed to be able to define `fix`

(via Kleene's theorem). So for example, in the case of `data Nat = Z | S Nat`

, `fix S`

is obtained as the limit of the sequence `⊥`

, `S ⊥`

, `S (S ⊥)`

, `S (S (S ⊥))`

, etc.

You do need to be careful about where the bottoms are. For example, in Haskell, `Maybe a`

is a DCPO consisting of `⊥`

, `Nothing`

, and `Just x`

for `x`

an inhabitant of `a`

. You can also define a strict variant:

```
data SMaybe a
= Nothing
| Just !a
```

which as a DCPO contains `⊥`

, `Nothing`

, and `Just x`

for `x`

a **non-bottom** inhabitant of `a`

. In particular, the sequence `⊥`

, `Just ⊥`

, `Just (Just ⊥)`

, etc. is no longer well-defined (or if you really want to give it a value, it would be constantly equal to `⊥`

), so you no longer get a way to construct an infinite sequence of `Just`

, and indeed the initial algebra (least fixed point) of `SMaybe`

only contains finite sequences of `Just`

/`S`

applied to `Nothing`

/`Z`

, and `⊥`

alone.

Note that this is not restricted to lazy languages. DCPOs serve just as well to model strict languages. It's just that there is an explicit distinction between values and computations which makes things more obvious in a way. For example, the option type in ML

```
type 'a option = None | Some of 'a
```

corresponds to the set of values consisting of `None`

and `Some x`

for `x`

in `'a`

. But the type `unit -> 'a option`

is not a pure function from `unit`

values to `'a option`

values. It is a function from `unit`

to computations with result `'a option`

. A computation with result type `t`

denotes an element of **the lifted type** `{⊥} + t`

(i.e., either bottom or a value in `t`

). So you can use `unit -> _`

as a type of thunks and encode everything that's going on in Haskell in a strict language.

- Haskell fails to infer the return type of a monad after using the sequence operator
- Does extracting values from a multiple Value return in Haskell invoke the function more than once?
- Why do I get "Unexpected reply type" from notify-send when using this Haskell notification server?
- Don't understand notation of morphisms in Monoid definition
- Foldln in haskell
- Is this property of a functor stronger than a monad?
- How to Instantiate a Custom Data Type with Record Syntax and Multiple Constructors
- How do I make a minimal working example for the a DBus server?
- Is it safe to downgrade Haskell stack version?
- Haskell, list of natural number
- unfamiliar syntax in Haskell / Clash function type signature
- foldM with monad State does not type check
- Why does my Runge-Kutta implementation oscillate to 0?
- How do I get the desired behavior in my TCP server?
- Why does the Haskell PVP describe new functions as non-breaking?
- How do I correctly use toLower in Haskell?
- How can I write a notification server in Haskell?
- Every Lens' is a Traversal'... how?
- How do I crate a value of type a{sv} for a call to org.freedesktop.Notifications.Notify via DBus?
- Web Scraping With Haskell
- Double exclamation marks in Haskell
- Haskell Servant POST FormUrlEncoded for (Vector String) field
- Confusion about list types in Haskell
- Idiomatic way to define new vs persisted types in Haskell
- Why does Cabal, unlike GHC, not automatically enable GeneralizedNewtypeDeriving if I explicitly enabled DerivingStrategies?
- What is the proper way of wrapping an Int (not a general type) in another type if type safety is the only motive?
- Parsing inside `between` with Megaparsec
- takeWhile implementation in JavaScript - Looking for better ideas
- How to setup MINGW environment variables for Haskell language server in vscode?
- mysql-haskell no invoke of Right case of try function