Lambda Cube

https://en.wikipedia.org/wiki/Lambda_cube

by Cieplak • 7 years ago

139 53 7 years ago

en.wikipedia.org

kuwze2• 7 years ago

"Each dimension of the cube corresponds to a new way of making objects depend on other objects"

Is it normal to refer to data structures as objects? Just to my knowledge most typed languages abhor the awesome potential of object-oriented programming, like the CLOS.

betterunix22• 7 years ago

In this context I think it refers to mathematical objects, since the dependencies can be between either values or types in either direction (values to values, types to types, types to values, values to types).

Also, lexical closures in a functional language are "classes" from the OO setting, so it is natural to implement classes if you want them; see e.g. OCaml. What you rarely see in the functional setting are common OO design patterns, because many of those patterns are unnecessary or awkward in functional languages.

Jim_Heckler• 7 years ago

Could you explain what you mean by closures being classes? My only familiarity is from Emacs/Common Lisp and Clojure.

kuwze2• 7 years ago

Thank you, I never knew how ignorant I was about that.

mruts• 7 years ago

I think Scala does a good job of unifying OO and FP. And because of everything being first class, you get to eliminate all the ridiculeous design patterns and end up with a very nice FP system based upon objects and traits or typeclasses

simiones• 7 years ago

I don't think you meant to imply this, but for anyone else - please note that the reverse can also be said - closures from an FP setting are objects from an OO setting, and it is natural to implement closures if you want them; see e.g. C++ "functors".

That is, objects and closures can both be implemented in terms of the other, if your language doesn't happen to offer both.

afpx• 7 years ago

“Mathematical Objects”: https://en.m.wikipedia.org/wiki/Mathematical_object

chriswarbo8• 7 years ago

I think this is the mathematical/logical distinction between "object level" and "meta level".

The meta level is about lambda terms, involving things like variable names, abstractions, judgements, derivations, equivalences, reductions, substitutions, etc.

The object level is what lambda terms are about, involving things like values, types, variable contents, etc.

igravious• 7 years ago

It's type theory, so the `objects' in question are either systems of terms and/or types. See where it says:

    terms allowed to depend on types, corresponding to polymorphism.
    types depending on terms, corresponding to dependent types.
    types depending on types, corresponding to type operators.

So I think they're using the word `objects' either loosely (as in, they could have said `things' but maybe that's too informal?) or they're using it as a shorthand for `type-theoretic objects', in which case they're talking about languages of a certain constrained expressive power: the language which features polymorphism, the language which features dependent types, the language which features type operator.

`object' here refers neither to the objects of object-oriented programming nor to object in common lisp object system.

edit: IANATT

Hackbraten• 7 years ago

Slightly disappointing. I wanted to learn about four simultaneous 24-hour days within a single rotation of the Earth.

wolfgke• 7 years ago

For those who do not understand:

https://en.wikipedia.org/w/index.php?title=Time_Cube&oldid=8...
https://ti.mecu.be/

HNLurker2• 7 years ago

https://www.youtube.com/watch?v=H7lWCqbgQnU

recursive3• 7 years ago

I know about Gene Ray. But I can't understand the actual lambda cube.

adamnemecek• 7 years ago

Reminds me a bit of the "Commutative diagram of harmonic wave" from wikipedia

https://commons.wikimedia.org/wiki/File:Commutative_diagram_...

mFixman• 7 years ago

Language theory and lambda calculus classes were some of my favourite in college. I wonder how many serious bugs would be averted if programming languages came with more complete type systems.

wespiser_20184• 7 years ago

You might think this: but there is a major time and complexity cost to using more advanced type systems that sometimes doesn't pay off in simpler applications that must ship fast!

dope99• 7 years ago

Can you support when this trade off ought to go one way or the other with any objectivity?

warent• 7 years ago

But the question is why "must" it ship fast? That seems to be a poor, irrational agreement we've made as a tech society for no better reason except because people are impatient.

chriswarbo8• 7 years ago

This is a common meme, but I'd like to see some robust empirical evidence either way (the only studies I've seen so far are with e.g. a handful of undergraduates, implementing a toy problem, well-specified up-front, with no maintenance/feature-drift/etc.)

As a trivial counterargument, there's nothing preventing programmers from ignoring even the most advanced type system (see "stringly typed programming", for example). In fact, my experience with "advanced type systems" (e.g. Agda, Idris and Coq), the types have never been a hindrance; it's their totality checking that can be painful (that's why Idris makes it easy to turn that off, either completely or for certain pieces of code).

wespiser_20184• 7 years ago

Re: Diminishing Returns of Static Typing: https://blog.merovius.de/2017/09/12/diminishing-returns-of-s...

neurotrace2• 7 years ago

I am currently checking in a fix due to a null reference exception. How I miss Option/Maybe when working in C#.

recursive3• 7 years ago

Nullable reference types in C#8 will help.

kvb• 7 years ago

Lambda Cube

Related Stories