Re: [Haskell-cafe] What's this pattern called?
I've often seen it referred to as the base functor for a recursive data type. You can then fix that functor in interesting ways i.e. with (Fix, Free, Cofree) and having the explicit base functor allows you to define general purpose recursion schemes over the data type. All of that extra machinery relies on your recursive data type being implemented as a functor with an explicit fixpoint, so base 'functor' seems quite appropriate. -Edward Kmett On Thu, Oct 22, 2009 at 3:47 AM, Martijn van Steenbergen mart...@van.steenbergen.nl wrote: Bonjour café, data ExprF r = Add r r | Sub r r | Mul r r | Div r r | Num Int This is a well-known pattern that for example allows nice notation of morphisms. But what is it called? I've heard fixed-point view, open datatypes and some others, but I'm curious where this pattern comes up in literature and what it is called there. Thanks, Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Thanks for all the pointers, guys. You've been very helpful. I also found Type-indexed data types (Hinze et al) to be a good source. Much appreciated! Martijn. Martijn van Steenbergen wrote: data ExprF r ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Hi Martijn, On Oct 22, 2009, at 9:47 AM, Martijn van Steenbergen wrote: I've heard fixed-point view, open datatypes and some others, but I'm curious where this pattern comes up in literature and what it is called there. Tim Sheard and Emir Pasalic call this technique two-level types in their JFP'04 paper Two-Level Types and Parameterized Modules: http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf Cheers, Sebastian -- Underestimating the novelty of the future is a time-honored tradition. (D.G.) ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
I've heard fixed-point view, open datatypes and some others, but I'm curious where this pattern comes up in literature and what it is called there. Tim Sheard and Emir Pasalic call this technique two-level types in their JFP'04 paper Two-Level Types and Parameterized Modules: http://homepage.mac.com/pasalic/p2/papers/JfpPearl.pdf Apparently from reading Section 2 of that paper, they would call ExprF non-recursive type the structure operator. I think, by itself, the type ExprF doesn't mean much. It really matters how it's used to determine what you call it. Martijn already mentioned the fixed-point view, but that only makes since in the context of something like Fix: data ExprF r = Add r r | Sub r r | Mul r r | Div r r | Num Int newtype Fix f = In (f (Fix f)) type Expr = Fix ExprF I believe the F suffix that Martijn used typically means functor, and I sometimes call types like this functors (with an optional but obvious instance of Functor). Regards, Sean ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Hi, On Thursday 22 October 2009 09:47:32 Martijn van Steenbergen wrote: Bonjour café, data ExprF r = Add r r | Sub r r | Mul r r | Div r r | Num Int This is a well-known pattern that for example allows nice notation of morphisms. But what is it called? ... The multirec package calls this the pattern functor (more accurately, it generates a sum-of-products-like higher order functor whose fixed point is isomorphic to your family of types, and calls that the pattern functor). -- Greetings, Daniel ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Conor also calls these functors: http://strictlypositive.org/slicing-jpgs/ The fixpoint construction builds recursive types (think trees) from functors by identifying superstructures with substructures: each node frames its children. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Obviously you are modelling the datatype -- data Expr = Add Expr Expr | Sub Expr Expr | Mul Expr Expr | Div Expr Expr | Num Int You already have ExprF, and now you need to throw in Fix newtype Fix f = In (f(Fix f)) in order to be able to build Expr like terms. type Expr' = Fix ExprF add a b = In (Add a b) sub a b = In (Sub a b) I've heard people refer to this technique of modelling datatypes as taking the initial algebra of the associated endofunctor (in this case ExprF) [http://strictlypositive.org/indexed-containers.pdf] This pattern is discussed in depth in Jeremy Gibbons work. I really recommend his Datatype-Generic Programming piece [http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/dgp.pdf ]. Someone else mentioned the multirec library. If you feel really adventurous you can look at the paper behind: Generic programming with fixed points for mutually recursive datatypes [http://people.cs.uu.nl/andres/Rec/MutualRec.pdf] or check out Andres presentation at ICFP [http://vimeo.com/6612724 ]. Just my 2c. On 22/10/2009, at 09:47, Martijn van Steenbergen wrote: Bonjour café, data ExprF r = Add r r | Sub r r | Mul r r | Div r r | Num Int This is a well-known pattern that for example allows nice notation of morphisms. But what is it called? I've heard fixed-point view, open datatypes and some others, but I'm curious where this pattern comes up in literature and what it is called there. Thanks, Martijn. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] What's this pattern called?
Martijn van Steenbergen wrote:
Bonjour café,
data ExprF r
= Add r r
| Sub r r
| Mul r r
| Div r r
| Num Int
This is a well-known pattern that for example allows nice notation of
morphisms. But what is it called? I've heard fixed-point view, open
datatypes and some others, but I'm curious where this pattern comes up
in literature and what it is called there.
This is an example of open recursion, which is when you take some
recursive function/datatype and rewrite it without recursion by passing
the function/type in as an argument to itself. It's the datatype
equivalent of doing:
fibF _ 0 = 0
fibF _ 1 = 1
fibF f n = f(n-1) + f(n-2)
fib = fix fibF
Which can be useful for functions because we can use a different
fixed-point operator, e.g. one that adds memoization abilities or other
features in addition to the recursion.
As others've mentioned, the open-recursive version of a recursive data
type happens to be a functor. Or rather, the recursive type happens to
be isomorphic to the least fixed point of a generating functor[1][2]
because the functor is also, in the terms of recursion theory, an
initial algebra. Part of why this pattern is so nice comes from the
fact that it's a functor (so we can use fmap to apply a function one ply
down), but part of it also comes from the isomorphism of using an
explicit fixed-point operator (which allows us to un-fix the type and do
things like storing the accumulators of a fold directly in the normal
constructors, rather than needing to come up with an ad-hoc isomorphic
set of constructors[3]), and the fact that it's an initial algebra ties
these two things together nicely.
This is also an example of Tim Sheard's two-level types, albeit a
trivial one since the fixed-point operator doesn't add anything other
than recursion. One of the particular ideas behind Sheard's two-level
types is that we can split the original recursive type in a different
place where one of the levels contains some constructors and the other
level contains other constructors. This can be helpful when you have a
family (informally speaking) of similar types, as for example with
implementing unification. All types that can be unified share
constructors for unification variables; but the constructors for the
structural components of the type are left up to another level. Thus we
can reuse the variable processing code for unifying different types, and
also be modular about the type being unified.
[1] This should be somewhat obvious if you're familiar with the
inductive phrasing of constructing the set of all values for some type.
E.g. Basis: [] is a list. Induction: (:) takes a value and a list into
a list. So we have some functor and we keep applying it over and over
to generate the set of all values, building up from the base cases.
[2] Do note that in Haskell the least fixed point and the greatest fixed
point coincide. Technically, whether the least or greatest fixed point
is used depends on the construction (e.g. catamorphisms use least,
anamorphisms use greatest). This is also related to the topic of
codata which is the fixed point of a terminal coalgebra.
[3] Data.List.unfoldr is a prime example of an ad-hoc isomorphic set of
constructors. Instead of the current type, we could instead use an
implementation where:
newtype Fix f = Fix { unFix :: f (Fix f) }
dataListF a r = Nil | Cons a r
typeList a = Fix (ListF a)
unfoldr :: (b - ListF a b) - b - List a
unfoldr = ...
which is a bit more obviously correlated with anamorphisms in recursion
theory.
--
Live well,
~wren
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
