Comments on: Rotten Bananas

By: The Comonad.Reader » Free Monads for Less (Part 2 of 3): Yoneda

The Comonad.Reader » Free Monads for Less (Part 2 of 3): Yoneda — Fri, 24 Jun 2011 04:50:06 +0000

[...] up once previously on this blog in Rotten Bananas. In that post, I talked about how Fegaras and Sheard used a free monad (somewhat obliquely) in [...]

By: Edward Kmett

Edward Kmett — Wed, 13 Oct 2010 13:55:57 +0000

Same thing, different authors, different words. =)

Difunctor often means the same thing as bifunctor, sometimes it is also used to denote a bifunctor that is contravariant in its first category. One use of this terminology is to describe a dinatural transformation.

Sadly there is little consistency in this regard.

By: Paul Keir

Paul Keir — Wed, 13 Oct 2010 13:24:24 +0000

Can you help me with some terminology? You mention that Hutton and Meijer derived a kind of catamorphism for exponential functors. Yet in their paper, they instead talk only about difunctors. They refer to this difunctor as coming from a paper by Peter Freyd: “RECURSIVE TYPES REDUCED TO INDUCTIVE TYPES”. I downloaded that paper, but it doesn’t mention difunctors, and instead discusses bifunctors. (Also, the Hutton/Meijer difunctor looks a lot like the bifunctor from your category-extras package.)

By: Edward Kmett

Edward Kmett — Mon, 04 Oct 2010 17:16:01 +0000

@Paul:

Very likely.

I’ll locate a more recent link and update the article.

By: Paul

Paul — Mon, 04 Oct 2010 09:04:32 +0000

Another excellent post.

I think some links may have died. I assume the 1996 Leonidas Fegaras and Tim Sheard paper is “Revisiting catamorphisms over datatypes with embedded functions (or, programs from outer space)”.

By: The Comonad.Reader » Unnatural Transformations

The Comonad.Reader » Unnatural Transformations — Sun, 27 Apr 2008 00:38:00 +0000

[...] Note that while 3 ‘Functors’ e, f and g are involved, only f needs to be a Functor in Hask because we do the duplication, hylomorphism and join all inside f in either case. And most of the time e = f = g. For instance e or g could be exponential or contravariant. [...]

By: Darin Morrison

Darin Morrison — Sat, 05 Apr 2008 12:00:22 +0000

The idea behind the Beluga project is to develop a dependently typed functional programming language that supports HOAS in a natural way. The connection to LF is that the Beluga language is split into two layers — a data layer which combines LF with constructs from contextual modal type theory in order to encode (open) data objects (which could represent terms in an object languages with binding described by HOAS), and a computation layer where things like recursion and case analysis happen. In Beluga, LF objects serve the same purpose as (G)ADTs in Haskell.

HOAS has been with LF and Twelf (which is just an implementation of LF + a logic programming engine and some other stuff) from the beginning, and Beluga has nothing to do with that specifically. What Beluga is trying to do that is new is to solve the problem of practical functional programming with HOAS. Compiler construction would be an obvious application.

In any case, it doesn’t really help you program easily with HOAS in Haskell… :)

By: Jim Apple

Jim Apple — Tue, 25 Mar 2008 19:51:06 +0000

It’s true that the goal of the project is different. The similarity I mean is that HOAS has *traditionally* had the problem of trading case analysis for safety. That is to say, it’s not a just a Haskell problem.

By: Edward Kmett

Edward Kmett — Tue, 25 Mar 2008 19:14:33 +0000

The Beluga project seems to be focused on the idea of how to represent HOAS in logical frameworks like LF, TWELF, etc.

My main focus is on using HOAS practically in a compiler in Haskell. Consequently, I wind up with a fair bit less control over exotic terms, because I don’t get to roll nearly as much of my own structure in the meta-language.

As a result I’m not sure how much what the Beluga folks are doing really helps, beyond the fact that it was fun getting a chance to pick at another HOAS encoding over lunch.

I had hoped that the Washburn/Weirich encoding would give me a ‘no exotic terms other than bottom’ security blanket, but it appears that I just have to suck it up. =)

By: Jim Apple

Jim Apple — Tue, 25 Mar 2008 10:32:25 +0000

I think the Beluga project (http://www.cs.mcgill.ca/~complogic/beluga/) addresses your issue. The first paper listed on the page is titled “Case analysis of higher-order data”. :-)