6

Collapsing Types vs Monads (followup)

 3 years ago
source link: http://twistedoakstudios.com/blog/Post4130_collapsing-types-vs-monads-followup
Go to the source link to view the article. You can view the picture content, updated content and better typesetting reading experience. If the link is broken, please click the button below to view the snapshot at that time.

Collapsing Types vs Monads (followup)

posted by Craig Gidney on June 4, 2013

Last week’s post about an automatically flattening future type received a lot of feedback. One of the running themes in the discussion was how collapsing types relate to monads:

“Type operators that collapse when you nest them inside of themselves”, along with some conditions to actually work as you would expect, precisely describe the idea of monad.

gasche

[…] This is the textbook definition of a monad.

PasswordIsntHAMSTER

monads, anyone?

cheng81

So the article and discussion here bring up a key question: what are the monads such that m (m a) and m a are isomorphic?

sacundim

Given the mix of confusion and interest, I want to clear up how monads relate to collapsing types.

Different

Collapsing types aren’t the same thing as monads, and neither is a subset of the other. They are attributes that can apply independently.

A collapsing type is a type that satisfies the property that nesting it inside itself has no effect. A Foo^{*}(Foo^{*}(T)) must act identically to a Foo^{*}(T) under all circumstances, for Foo^{*} to be a collapsing type.

A monad is a type that supports three operations: wrapping, transforming, and flattening (more typically called return, fmap, and join respectively). The operations must also satisfy a few work-in-the-obvious-way-please rules.

If you tell me that Foo^{*} is a collapsing type, I still don’t know if the type supports the operations necessary to make it a monad. Collapsing types technically support flattening, in that a proper join method doesn’t have to make any changes. However, collapsing types are not required to support wrapping or transforming.

Conversely, if you tell me that Bar is a monadic type, I still don’t know if it satisfies the condition join_{Bar} = IdentityFunction needed to qualify it as a collapsing type. Monads are not required to have join operations that change nothing.

Examples

There are non-collapsing non-monadic types, collapsing non-monadic types, non-collapsing monadic types, and collapsing monadic types. Just to really drive home that “collapsing” is separate from “monadic”, lets go over an example of each.

An example of a collapsing monadic type is Future^{*}, from last week’s post.

An example of a non-collapsing monadic type is List. You can wrap anything into a list, transform the items in a list, and flatten lists of lists but a list of lists of integers is not the same as a list of integers.

An example of a collapsing non-monadic type is a Remote type representing an unknown value stored on a remote server, where the details of the server potentially using a further-remote server are hidden (meaning you treat a Remote(Remote(T)) exactly like a Remote(T)). If the server doesn’t allow you to apply arbitrary operations to remote values, or create arbitrary remote values, then Remote is not a monad.

An example of a non-collapsing non-monadic type is SquareMatrix. It’s not a collapsible type, because a matrix of matrices of booleans is distinct from a matrix of booleans. It’s not a monad unless you specify a flattening operation, but you’ll find there aren’t any nice ones to pick because you can’t preserve the number of values. For example, properly flattening \left| \begin{array}{cc} \left| 0 \right| & \left| 1 \right| \\ \left| \begin{array}{cc} 2 & 3 \\ 4 & 5 \end{array} \right| & \left| 6 \right| \end{array} \right| would require that seven be a square number (it’s not).

Side note: Technically you could make SquareMatrix into a monad by specifying a poor flattening operator, and so you might be tempted to say SquareMatrix is a monad. Don’t do it. Under that view, every type ever is a monad. Given a type T, you can make it a useless monad by picking a value v of type T and defining join, fmap and return to all unconditionally return v.

Similar

Monads and collapsing types are different, but still related.

In practice, collapsing types you encounter will probably be monads. Mainly because most of them will be related to eventual results (e.g. promises/A+ in JavaScript, Twisted Python in Python, ppltasks for windows store apps in C++).

In theory, you can start from any monad Foo (which may not be a collapsing type) and derive a related collapsing+monadic type Foo^{*} by making the application of join automatic. It’s what I did with Future last week. All the methods on Future^{*} did internal checks to see if flattening was necessary or not, to make a Future^{*}(Future^{*}(T)) act exactly like a Future^{*}(T). This derivation makes more practical sense with some types (Future, MayHaveFailed, Observable, MayHaveCancelled) than it does with others (Nullable, List, Tree, Parser).

Warning: a potential issue with the above derivation is the creation of self-referencing flattening cycles, where you end up with a type nested inside itself infinitely many times and keep trying to unwrap it. For example, adding the following three lines to my collapsing future’s python fiddle causes a flattening cycle:

cycle = Future()
cycle.trySetResult(cycle)
cycle.continueWith(out) #never halts

It’s probably a good idea to have runtime checks for this issue. Compile-time checks would be even better, but beware accidentally solving the halting problem.

Summary

Collapsing types are not the same thing as monads.

You can transform any monadic type into a collapsing monadic type.

Next week: less type theory.

Discuss on Reddit

Comments are closed.


Twisted Oak Studios offers consulting and development on high-tech interactive projects. Check out our portfolio, or Give us a shout if you have anything you think some really rad engineers should help you with.

Archive


About Joyk


Aggregate valuable and interesting links.
Joyk means Joy of geeK