Lambda the Ultimate

Mwa. That you can do continuation passing in monadic style seems a no-brainer, since you can do everything^tm in monadic style. It looks to me Meijer thought of something different, or the question didn't make it right to the article.

0 points so far! (In Eurosongthingy style.)

The interview question is to provide "bind" and "return" operators for the parameterized type (Cont r) type, and check that they satisfy monadic laws. "bind" is indeed not obvious.

return : a -> Cont r a
bind : (Cont r a) -> (a -> Cont r b) -> Cont r b

I am worried by the amount of incomprehension category theory that you displayed in the FRPnow thread -- because it is not conductive to productive discussion and does not make LtU a better community to be part of. dmbarbour is not always easy to follow but his answers make sense to me. Yours do sometimes, but when "monads" or "category theory" are on the table they don't anymore. You could invest some time into learning about them; you have publicly said that you did not plan to, and this is just fine. But if you don't understand them and don't plan to invest more work into understanding them, maybe it would be best for you not to talk at length about them.

Yeah right.

It's an interview question. Even so-called "no-brainers" like FizzBuzz can often filter a depressing proportion of candidates.

Showing Cont is a monad by defining return and bind (and thus showing knowledge of monads and type analysis, etc.), or pointing to the MTL library (and thus demonstrating one's knowledge of the problem and the available resources, and a healthy habit of looking up existing answers before reinventing old wheels)... either would probably be an acceptable answer in context of an interview. Though the latter is more dubious by far, and my answer was hence rather tongue in cheek.

I certainly wouldn't bet on most people passing. :(

As gasche mentions, the definition for `bind` is not obvious. (It is simple, though.)

No, I could have come up with those definitions. I understood the question in a different manner. I.e., show that that type is isomorphic to a monad and satisfies monad laws.

The type is not isomorphic to a monad, as a monad has a type like this:

(forall a b . m a -> (a -> m b) -> m b, forall c . c -> m c)

What you want to show is the type can be substituted for 'm' in the above, and you can show that satisfies the monad laws.

Maybe I am focusing too much on the words and not the intent, I get what you mean, I just think words are important, certainly my compiler keeps complaining about the words I use in programs all the time :-)

No, that's exactly why I found the assignment puzzling. I supposed that since continuations and monads are much alike, roughly something like control operators, the aim of the game was to show isomorphism.

But the only requirement was to show that there are unit and bind operators. I don't assume that by doing so we have shown isomorphism?

(Actually, Erik uses the terms 'forms a monad'.)

Douze points

I wonder if LtU would be better or worse with voting. What we have is a nice balance between the linearity of a forum and Reddit-style threaded discussion.

But at the same time, you run the risk that all dissent is down-voted. And I am not that happy with LtU. I sometimes wonder whether what is published here should not be seen as masterpieces but medals for sheer incompetence. That is, no relevant news from industry and, personally, I am of the opinion that these days all relevant research is in industry and academia is mostly busy with some self-serving navel gazing.

Where's the latest news on C++, untyped languages like Python and Ruby, machine learning, or compilers targeting Google's tensor hardware?

(Anyway, it's a bit of a joke. It's Eurovision songfestival time, and this is the highest grade. You can Google it.)

Providing the full stepwise proofs of monad laws? In an actual interview, you'd likely get extra credit for even thinking to​ do so. And then you'd probably be stopped so they could move to another question.

I’m familiar enough with this stuff at this point that the slow part is the physical act of writing it out.

I think this is what the interviewer was looking for. Just defining unit and bind does not make something a monad, those definitions have to have a left identity, a right identity, and be associative.

Edit: OOPS! Sorry I shouldn't have posted an exercise from memory. This wasn't supposed to be hard, but when I tried to do it I got stuck. I forgot I need the return type of the continuation to be in the monad, too. And the quantifier over the return type isn't necessary -- it should probably be left a parameter as with Cont.

FIXED PROBLEM:

Show that for any monad m with bind and return (with correct types but satisfying the monad laws or not), you can define bind' and return' making the following type into a monad (satisfying the laws even if m didn't):

type CPm r a = Cont (m r) (m a)

If you're once bitten, twice shy and don't want to spend any more time on my nonsense, I'll post a solution tomorrow.

Hmm. I passed my algebra exam twenty years ago, so I am slow, but I bet it's just the same trick for introducing a unit' (by also using unit) and then deriving a bind' which looks mostly similar but also employs bind to chain stuff together.

That doesn't look too hard but I'll gladly leave it to others for now.

Edit: Something like?

unit' = λx k. k (unit x)

And the rest follows naturally? Hmm, it's 4:30am here. Tomorrow, maybe.

It wasn't supposed to be hard, but I suspect it may have been ... quite challenging... due to the fact that I bungled the problem statement. See above.

It doesn't look hard. Just another algebra exercise where you need to introduce and chain stuff together. But I want to know more about some SMB worm at the moment, so I'll take a raincheck.

Sorry because my initial phrasing of the problem was wrong and probably impossible. But if you're not interested I'll skip the solution. You're right it's not hard. Very similar to the above from Jon.

Interested enough to wanna know whether my initial estimate of unit' was right. And I guess you need to use a bind in bind'.

But I forgot how Haskell works so I would need to check everything by hand, instead of just running the type checker on it, which is too tedious enough for me.

I'm mobile today so can't check either but I think your unit' is right. I think bind' should be:

bind' m k c = m \ma. bind ma \x. k x c

Ran g h a = forall b. (a -> g b) -> h b 

Cont r a = Ran (Const r) (Const r) a 
Codensity m a = Ran m m a

Cont a = Ran Id Id a

forall b. (a -> b) -> b

Thanks for the connection.

The "Yoneda Lemma" (which is a kind of church encoding of a functor) is another special case:

forall b. (a -> b) -> f b  

which corresponds to:

Yoneda f a = Ran Id f a

And ofc there's a dual "Left Kan Extension":

Lan g h a = exists b. (g b -> a) (h b)

with its corresponding "Cocontinuation", "Density", and "Coyoneda"

Wondering whether if you walk up the hierarchy of abstract nonsense you'll just end up with one combinator/functor which will do everything? That's how combinator rewriting ended, one combinator and one axiom which does 'everything'.

Just like if you put a monkey with a typewriter in a closed room, given enough time and lifespan, the monkey would end up with all of the Shakespeare greatest books written by himself. Of course, among all of the other combinations. The problem is that there are so many combinations that we could never pick the interesting ones.

The same goes to a type system. A type system describes all of the possible algorithms that can even exist. If we start enumerating them, one by one, we would end up with a lot of artificial general intelligence algorithms. One of the algorithms would be the most wonderful AGI personality one can imagine. And the other would be the most mean AGI personality one could imagine. So, finally, maybe it is good thing that this mean personality is hidden behind 2ⁿ combinations. We loose the good one, but it is enough safe not to get the bad one.

A type system describes all of the possible algorithms that can even exist.

Surely not. (Sorry to intrude on the thread.) Most type systems are about excluding vast swaths of algorithms.

You can come a long way with integer arithmetic, so as long as your type system allows that, you don't exclude anything.

Type int->int suggests ability to write all computable functions. My interpretation of the word "algorithm" is about how things are computed rather than merely what they compute.

We can write an interpreter for Turing machines (or your favorite model of computation) in Turing-complete typed languages; would that not give completeness for the notion of algorithm that you have in mind? Even among the strongly normalizing calculi, we have rather strong results -- you have to sensibly weaken linear logic to get something that captures polynomial algorithms only, and System F is complete for any complexity class I've ever heard algorithmicians being interested in.

... and System F is complete for any complexity class I've ever heard algorithmicians being interested in.

A Turing tarpit is a Turing-complete programming language in which any computable function could theoretically be written, but in which it is impractically difficult to do so.

System F (without non-termination extensions) is not Turing complete, but yes, the fact that its termination bound is humongous means that most algorithms can be expressed (if one is into set theory, there was a paper this year expressing System F normalization strength through (a variant of) bar recursion), but not that it is convenient to express them in this form.

Both ML-family languages and Haskell go beyond System F in day-to-day programming, with modules in ML and higher-kinded type constructors in Haskell, that both belong to the stronger language F-omega.

There has also been interesting research on expressivity of languages capturing more restricted computation classes, see for example Pure Pointer Program with Iteration, Martin Hofmann and Ulrich Schöpp, 2008, which proposes a programming language for a strict subset of LOGSPACE that is more expressive than previous approaches. The point is that even with languages designed for restricted complexity (which are a special sort of strongly-normalizing languages), our understanding of the question of expressivity/practicality is often fine-grained, people went past the mere idea of a tarpit.

People in complexity theory might study different classes and have nuanced feelings about the tarpit but I don't really feel the inclination to follow them in that. I just want languages which allow me to more or less directly state pure or impure textbook algorithms. (Though my own language is an eager untyped term rewrite system.)

Not really my thing. Not worthless either.^1 Although the remark that ML and Haskell implement F-omega variants I find a bit of a stretch. But I haven't looked at Haskell's type checker for ages.

^1: Edit. That came out wrong, I was thinking what it would mean for my term rewrite language.

May I ask what is the difference between functional programming and term rewrite system?

It depends on who you ask, I guess. If you go really broad and see functional programming as a programming style even C is a functional language, and if you go really narrow only languages like Haskell are.

I call it a term rewrite system because even the runtime system I implemented in a bit of an old-school manner tries to remain as faithful to a term rewrite system as possible. Although I turn the term inside out to get some performance out of it.

... I need to learn a new word today :)

How would we call "algorithms" in functional languages? A function composition? I kind of liked the word "algorithm", it had a kind of cool electronic echo in my mind.

Terms?

a better idea: a computing unit! Kids would love it! B]

[edit] No? Ok, term it is.

Yah, maybe that was a silly remark.

Roughly, if you look at the relation between types and terms, you should have

• Lambda terms which are interesting and which cannot be typed in a type system X.
• Typed terms in type system X which are uninteresting because they don't encode any useful algorithm.

I don't think it is hard to have a type system that can type any lambda term, although I don't have a proof, I used random open lambdas to test my type inference algorithm. "Compositional Principal Typings" with recursive types enabled can infer a type for any lambda expression I have been able to generate.

However, I am not convinced of the usefulness of this approach, after all, if you can type any term, what safety does it give you? Yes, you could use the type system to add type-classes and generic types to a language with type inference, but the type of most complex lambda terms devolved into something like: "mu A . A -> A"

What would the point be of a type system that could type any lambda terms? The whole point of the game is to exclude terms?

A possible use for being able to type everything is to detect useful terms which aren't typeable in another more restricted system, I guess.

I failed to mention that type systems also often exclude types which are interesting, syntactically valid, but don't meet the type system's criteria.

My pet peeve interesting type is

type automaton i o = i -> (o, automaton i o)

This fails to type check in lots of systems.

It seems to me, intuitively, that any type system must either exclude terms that are of interest, or include terms that are wrong, even if there were a clear dichotomy between the two kinds of terms (which, on consideration, there might not be). This feels more like an informal principle than a formal hypothesis, but at a minimum, if one chooses some particular class of actions to define as "wrong", the set of programs that would actually do those things is undecidable, whereas presumably a type system is only useful if typing of terms is decidable.

I think they moved away from decidable type systems (in the general sense) and moved towards 'in general decidable with a little help' because the former was too restrictive.