Lambda the Ultimate

I have a typeclass just like that in my prelude.

The only thing is, unless I am missing something, I think the instance needs to be:

instance (FI a, FI b) => FI (a -> b)
    ...

In practice it works pretty nicely, because when functions really are simple you can get a tabular version for documentation very, very easily.

I split it up, though, because its possible for (countably-) infinite types to belong in the enum "half" of that typeclass.

Other fun goodies you get are things like

class Finite a
    count :: a -> Natural -- pass me undefined, but my parameter needs to be here so that we know which count we are talking about :(

class Enumerable a
    fromInteger :: Natural -> a
    toInteger :: a -> Natural


-- in the monad of random variables
uniform_distribution :: (Finite a, Enumerable a, RandomGen g) => a -> Rand g a
uniform_distribution a = do
                           n <- getRandomR (0, (size a) - 1)
                           return $ fInteger n

There's an unenforced law that when something is both enumerable and finite that its fromInteger works on [0, count-1] and its toInteger produces results in [0, count-1]. I'm not thrilled by this rule because its not clearly part of the contract of Finite nor is it clearly part of the contract of Enumerable. Anyone got a better idea?

I'm also not thrilled by the (undefined :: DayOfWeek) that you have to pass to uniform_distribution so that it can pass it to size, but I'm not sure if there is anything to be done about it. I think there is some trick to be pulled with using type-level naturals to encode the size.

Even further down the rabbit hole, maybe it should really be a type-level cardinal, and the type function Cardinality :: * -> K^cardinality is defined at every type in *?

AFAICT you also want the instance:

instance (FI a, Data b) => Data (a -> b)

In addition to:

instance (FI a, FI b) => FI (a -> b)

This is what I intended with my last hurried post.

(Oops, this was a silly question.)

*head explodes*

So, yes, functions are codata, and they correspond to infinite memo tries in a systematic way, whenever the domain can be considered a set of finite paths.

It'll take me a long time to wrap my head around this whole thread, but the possibilities are enticing. I think the first time I made a flimsy connection about this relationship, ie. functions=codata, was in the finally, tagless paper, where they said that the lambda calculus had a coalgebraic structure. When I read that, I reasoned that if data=algebra, then functions=coalgebra implies function=codata.

I still don't understand the full implications, but this thread has highlighted some possibilities. For instance, if functions=codata=infinite memo tries, then is compilation the construction of such a trie from a function definition, ie. the trie is the executable instruction stream with edges being branching instructions?

By "finite paths", do you mean the domain is a non-recursive or structurally inductive algebraic type? That would make sense, at least for non-recursive algebraic types would elaborate into a sequence of instructions with a finite number of branches as a trie.

Jan Rutten has been thinking and writing about this for a very long time -- but somehow few people in the FP community seem to be aware of his work, or 'mining' it appropriately. Look at his papers, especially the ones from the late 90s. My personal favourite his his 2003 TCS paper on behavioural differential equations (i.e. defining streams up to behavioural equivalence via differential equations).

What Conor is pointing out can be generalized: there is an isomorphism between S () -> x for any species S (considered as a type constructor) and codata T x where T x ~= x^{S ()}. The isomorphism works because S is graded, so the molecular decomposition of S as an infinite series translates to an infinite product for T. The most complicated thing (which is not entirely obvious from the above code) is that the labelled product 'Node Tree Tree' translates to Functorial Composition, aka 'Bush (Bush x)' - and I do not know how to do this systematically.

More specifically, what I don't know how to do is to take either the algebraic equation, or even better, the corresponding differential equation, and translate it systematically to a useful (algebraic or differential) equation for Bush. In this case, x Bush' = Tree * Bush, but how do I "integrate" this to get Bush(x) ~= x*Bush(Bush(x)).

Apologies for what's probably a dumb question, but can you explain where you got the following equation?

x Bush' = Tree * Bush

On the other hand, it looks like Conor's equation for Bush follows in a straightforward way from the goal of being isomorphic to Tree -> x:

Tree = 1 + Tree²

Bush x

= x^Tree

= x^{1 + Tree2}

= x * x^Tree2

= x * (x^Tree)^Tree

= x * (Bush x)^Tree

= x * Bush (Bush x)

I differentiated the equation
Bush x = x^Tree(x)
which gives
Bush' x = Tree(x) x^(Tree(x)-1)
then multiplied both sides by x (so as to not need virtual species), and then refolded the definition.

Thanks a lot for that derivation of the Bush equation -- I had not seen that. I do believe that your derivation does contain some key ingredients to prove a more general version of this idea.

Ok, your differential equation was derived from the original equation. I should have tried that, but I thought you might have had some way to write it down directly.

As an aside, one thing that bugged me after posting that derivation was that it didn't seem to use at any step that Tree is inductive. If we take (Bush x) to be defined as (Tree -> x), then all of those steps are valid for any Tree that satisfies the Tree equation, data or codata. But the correspondence between (Tree -> x) and the codata version of Bush only holds if Tree is inductive, so what gives? The answer is that the re-write rule of the derivation above is only justified in being applied finitely many times. If we instead start from the desired coinductive definition of Bush, then the last two substitutions will need the inductive hypothesis for justification.

I agree there's probably a more general version of this, but Conor's other example, μx. β + (α → x) = Stream α → β, doesn't seem to have the same flavor as the Bush/Tree example. Starting from Foo α β = Stream α → β, it seems that we need to rely on the parametricity of Stream α → β to make progress. Anyone know how to do this?

It would be quite instructive to do this inside a proof assistant, to really see what assumptions are needed. Of course, this may well be at the very edge of what proof assistants can handle comfortably (i.e. one might run into all sorts of limitations of Coq and/or Agda which are not otherwise a problem in the theory itself).

And while I claimed "more general", I just meant up to (Species -> x), not more than. Like you, I am quite sure that there is indeed a 'higher algebra' of this which would cover Conor's example, but it is much trickier. One can easily unwind μx. β + (α → x) to β + β^α + β^α2 + ..., and Stream α → β to β^αNat, but these are not isomorphic! The condition that makes it work is that continuity forces one to take a strictly finite amount of information from Stream α, and then we have the isomorphism. Note that I believe it is continuity, not parametricity, which makes this work -- but I would be happy to learn that these are somehow tightly related.

The step I don't see is "then we have the isomorphism." I think the reason is: those types aren't actually isomorphic (even in the case β is data). The type μx. β + (α → x) encodes more information: if you have such a type, then you get to observe how many steps were required to produce a β.

BTW, my suggestion that we use parametricity was nonsensical. Sorry.

I read Conor's 'isotope' as isomorphic data type, but perhaps it's a reference to an isotopic data type? I'm familiar with isotopy from topology, but I don't really see how that concept would apply to a pair of data types. Is it possible the data types are isotopic but not isomorphic?

Also, I made a minor edit to the parent post for clarity.

By "isotope", I do indeed mean "isomorphic type", but in somewhat loose and informal sense here. That said, there's more than a whiff of topology to what's going on, with all the connections between computability and continuity.

Fair cop, I did rather skip whistling over a bump when I switched from coding functions with finitary domains (where it's clear how to implement both directions of the iso directly) to functions from codata. For the latter, it's easy to interpret the codes as functions, but it's rather trickier to extract the code from the function.

So what's the status of the claim? One needs rather stronger reasoning principles to show that every total function has a code than you get just by being able to apply functions to codata. That's distinctly meta. You need to ask "what can this function possibly do with its input?".

Having said that, if we define

  {-co-}data Stream a = a :> Stream a 
  data Eater a b = Return b | Eat (a -> Eater a b)

I bet we can use some deep wickedness to implement a Haskell function

  encode :: (Stream a -> Bool) -> Eater a Bool

which will indeed produce the code. When I say wickedness, I mean using unsafePerformIO to embed effects in the input to the stream-consuming function which interact with an element supply.

Which is all to say that these more concrete characterisations of functions from codata are really external observations on computability, but that they can be realised if you have some means to spy on the machines.

I agree with all of the above. My hangup was looking for an actual isomorphism, when in fact the type μx. β + (α → x) can encode Stream α → β, but not vice versa. E.g. the following Eaters correspond to the same Stream function:

foo = Return False 
foo' = Eat (\a -> Return False)

That's a fair point. We get that every computable function has an encoding, and we can get hold of that encoding if we can do some sort of intensional observation of the function. But extensionally speaking, we might get multiple (clearly, infinitely many) encodings for the same function.

If I want to legitimize my use of "isotope" in these examples, as well as define the things computationally, then I need to consider functions from codata up to the finer equivalence induced by the more intrusive observations (e.g., applying functions to booby-trapped inputs and detecting the kaboom).

import Prelude hiding (catch)
import Control.Exception
import System.IO.Unsafe
import Control.DeepSeq

data Stream a = a :> Stream a
data Eater a b = Ret b | Eat (a -> Eater a b)

encode :: NFData b => (Stream a -> b) -> Eater a b
encode f = unsafePerformIO $ let b = f (error "Kaboom!") in
  catch (b `deepseq` return (Ret b)) $
    \ (ErrorCall "Kaboom!") ->
    return . Eat $ \ a -> encode (f . (a :>))

Sorry, NSFW, I know...

Nicolas Oury and I just implemented encode in SML/NJ using Filinski's encoding of shift and reset:

datatype 'a Cons = C of 'a * 'a Stream
withtype 'a Stream = unit -> 'a Cons

datatype ('a, 'b) Eater = Ret of 'b | Eat of 'a -> ('a, 'b) Eater

fun tryOne () = shift (fn k => Eat (fn a => k (C (a, tryOne))))
fun encode f = reset (fn () => Ret (f tryOne))

This has the advantage of running f only once. It even works correctly with side-effects in f :-)

Yes, that's what I *really* wanted.

I took me a little while to recognise that familiar seeming computation. I have at least one generalisation there.

E.g., μx. β + (α → x), being the free monad on the ‘read an α’ command, is an isotope of Stream α → β when the elements of β are finitary.

Why do you say that the elements of β need to be finitary? I did an implementation and it seems quite irrelevant what β is.

Take β to be Stream α. Express the identity function.

Clear. Thanks!

The same transformation on Stream a -> Stream b gives you a well-known coidinuctive type: the Stream Processors.

We implemented that using shift/reset in SML, following up on our previous post:

datatype 'a Cons = C of 'a * 'a Stream
withtype 'a Stream = unit -> 'a Cons

datatype ('a, 'b) SP = 
         Put of 'b * (unit -> ('a,'b) SP)  
       | Get of 'a -> ('a, 'b) SP

fun probeOne () = shift (fn k => Get (fn a => k (C (a, probeOne))))
fun emitOne s = 
   let val C(v, s') = s() in
     shift(fn k => Put (v, k));
     emitOne s'
   end

fun encode f = reset (fn () => emitOne (f probeOne))