Circular Instance Declarations

[Brandon Michael Moore]

On Sun, 7 Sep 2003, Ashley Yakeley wrote:

> In article <Pine.GSO.4.44.0309072012230.3951-100000@blinky>,
>  Brandon Michael Moore <brandon@its.caltech.edu> wrote:
>
> > Detecting circularity in a derivation is equivalent to accepting a regular
> > infinite derivation for instances. Would you have a use for irregular
> > derivations?
>
> Could you give me an example?

I should have asked whether you needed irregular types, and "undecidable"
instances for irregular types.

I'm close to a proof that will justify more permissive instances for
regular types (plus a bit), but I haven't made much progress on irregular
types. I'm wondering if anyone actually uses them, let alone
fancy instances for them. Also, if I tried to expand my approach to
irregular types it would require generating dictionaries a runtime, rather
than just defining dictionaries recursively.

In case the word irregular is the problem I'll give my definition, and how
I'm applying it to types. The definition is from Pierce, in "Types and
Programming Languages".

An irregular tree is a tree with an infinite number of distinct subtrees.

When I say a type is irregular I mean the infinite trees you get when you
(recursively) expand all the applications of type constructors is
irregular.

A simple irregular type is
Irr a = Con a (Irr (F a))
(as long as F uses a)

This expands to something like <a|<F a|F (F a)| ...>>, where <t|t..t>
denotes a sum type. Each right child is like the parent with an extra F
everywhere, so the tree is irregular.

The sort of instance I'm interested in is something like
instance (Eq a,Eq (Irr (F a)) => Eq (Irr a)
where the context only mentions (subexpressions of) type expressions
encoutered while expanding the type.

Are you using anything like this?

Brandon