What is a not-well-founded cotree?

I'm reading the paper "Dual of substitution is Redecoration".
And I'm struggling with understanding the usage of the word "not-well-founded cotrees".

• what is a cotree compared to a tree ? I suspect it is a tree for which all relations are inverted, but it is just my assumption.

• what it is to be "well-founded" for a tree, for a cotree.

Probably, to have an insight, it would be helpful to give me examples of a well-founded and of a not-well-founded tree/cotree.

I'm not sure what you mean by "all relations are inverted" (what's the relation of a tree?), but perhaps I can provide some insight.

In Haskell, one might write the type of binary trees as such:

data Tree = Leaf | Node Tree Tree

in the terminology of the paper, the type of "incomplete trees" would then be

data ITree a = Leaf | Node ITree ITree | Var a

allowing for an "incomplete" tree with holes marked by an instance of Var a. The paper observes that the type ITree a forms a monad, where a Var a can be "substituted" with f a given a suitable function f :: a -> ITree b.

Now our intuition is that the type Tree is the type of finite, or well-founded binary trees, of which an example is

myTree :: Tree
 myTree = Node (Node Leaf Leaf) (Node Leaf Leaf)

However, it is untrue in a language like Haskell that all trees are of this form. Indeed, following definition is perfectly acceptable:

infTree :: Tree
infTree = Node infTree infTree

intuitively, this tree represents the infinite "full" binary tree. So really the type Tree may contain either finite binary trees, or trees which may contain infinite paths. Such trees are called non-well founded trees.

So, in Haskell, the type Tree is in reality the type of co-trees, which allows such elements as infTree. This may be a bit confusing, since we rarely think about such elements when considering that type.

Hopefully this provides useful intuition.

The main observation of the paper, is that the type of co-trees has a construction dual to that if ITree, which one might call DTree, defined as

DTree a = DLeaf a | DNode a (DTree a) (DTree a)

such that we can define a comonad structure:

extract :: DTree a -> a
extract (DLeaf a) = a
extract (DNode a _ _) = a

duplicate :: DTree a -> DTree (DTree a)
duplicate (DLeaf a) = DLeaf (DLeaf a)
duplicate (DNode a l r) = DNode (DNode a l r) (duplicate l) (duplicate r)

The paper goes on to explain some intuition about this structure and why it should be considered as interesting.

Oh by the way, the paper you are reading seems pretty heavy in abstract nonsense, and if you're coming from the CS side of things, you might want to take a look at these blog posts first:

https://bartoszmilewski.com/2013/06/10/understanding-f-algebras/

http://5outh.blogspot.com/2013/01/comonads.html

StackExchange Computer Science Q#92511, answer score: 4