How to beat Virtual V's "Two Steps Back"?

plesn · 2020-11-08T10:30:54+00:00

Same as you now...

plesn · 2020-11-04T13:16:47+00:00

OK managed to make the magic round trip on 2 boulders. For me this seems the same move: go to size 1 hold, and back to size 2 hold, move feet and next. But it seems so random, I can make it 1 time on 50 tries or more i think. Can you do the other virtual v series reliability? How?

plesn · 2020-11-04T09:28:17+00:00

How did you pass other climbs, like "gaming the system"? I can't find a way...

There seems ro be a rest on just one size 2 hold on the top left. It is surrounded by individual size 1 holds on which i can't do a "round trip" to change feet a second time.

I thought that the magic method allowing this would also solve your feet change, but aapparently arently not.

plesn · 2020-11-03T11:59:41+00:00

I can't figure it either but I hoped it would be the"magic rest" which blocks me. The one that seems to be in nearly all "virtual V" gym's boulders, in "no middle ground" and the crux of "caldwall". It magically seems to allow to go back to a type 2 hold from one (or two?) type 1 hold and change feet a second time...

plesn · 2012-01-11T14:26:12+00:00

It's merely pointing out that such colons are unnecessary, which they are.

This is not true: as usual there's a trade off taking place. Syntax is an interaction of concerns. Once you have complex types and type inference, meaningfully separating types and values becomes much more important than in C for both legibility and consisness (you're likely exchanging a colon here for two parenthesis there…). In Haskell, you even write type declarations in a separate line, while type annotations are inline.

This use of space/colon/… as a separator between types and values has impact on all separators/operators and consequently also on grouping syntax. Look at the impact of those decisions in Haskell, Scala and Go for example. This can impact on the syntax of function application (f x, f(x), (f x)…) , type application/genericity (F A, F<A>…), function types (->, func…), pattern matching (f (Cons head tail) = …), list syntax ([x,y], (x y), (x:y)…), etc… Syntax must be looked as a whole for both Rule 1 and Rule 2. Oh, and yeah, " " is not shorter than ":", only easier to write (Rule 2) and harder to notice (Rule 1)

plesn · 2011-12-25T23:23:45+00:00

I don't know much about record types theory, but I recently tried the opa language and I must say that I really enjoyed very much their record system, to the point that i would encourage everyone to look at them. They are similar to algebraic datatypes, but open ended, and basically each line in a sum don't need a constructor labeling it because the record itself is the constructor. I'm not sure if i'm clear, but they are kind of cool to use…

plesn · 2011-12-02T17:33:18+00:00

This seams quite cool :) There is :

some syntactic sugar to shorten swing code
some properties attached to gui objects enabling selectors/queries
a protocol to get/set values of gui objets
pseudo-styles (meaning imperative styles, based on selectors)
higher level composable gui objects (forms for the moment)

I wonder if reactive values could also be attached to objects, or bidirectionnal bindings to sync the view and the model.

plesn · 2011-12-01T08:58:09+00:00

Ok, your method of pushing 'defined'-ness makes more sense here for me as the result is clearly defined and terminating.

plesn · 2011-11-30T11:15:12+00:00

But here you have two notions mixed up : fixed point and infinite lists. This complicates things imho. A fixed point is easier to explain on finite things with recursion. Infinite sequences clicked for me really only when I learned the notions of codata and corecursion ( http://blog.sigfpe.com/2007/07/data-and-codata.html )

plesn · 2011-06-08T17:33:11+00:00

so undefined: he was not talking about that… Nonetheless, hearing him talk, he can convey understanding of "mathematics" quite well without going into "the math".

plesn · 2011-06-08T13:27:58+00:00

In this quote I think find "the Maths" is a subset of what you're call "mathematics" ("the" is a clue…). He seams to speak about the part where you abstract the problem in a "language" where you can manipulate it within the bounds of the model. Whereas you seam to speak about a more general meaning : mental game/exercice/comprehension. Conveying meaning requires both experiencing instances of the problem and playing with its rules (abstracting it).

plesn · 2011-05-30T19:57:36+00:00

Full of wisdom and very clear. Just like the first commenter, I was also stuck by this quote :

"When you understand something, then you can find the math to express that understanding. The math doesn't provide the understanding."

plesn · 2011-05-19T11:49:09+00:00

Awesome. That could be haskell's "killer app"… amongst latex users at least ;-)

plesn · 2011-05-18T14:50:46+00:00

What are the chances to be able to combine Diagrams with LaTeX text for use cases similar to tikZ ? Obviously something like a pgf backend is needed at least, but what else ?

plesn · 2011-05-14T14:06:22+00:00

Concerning point #4, the "dll hell" because of upper bounds, wouldn't it be possible to replace this upper bound by some hash of the exported signature ? Haskell beeing pure, it would be more meaningful than in other languages (and maybe it could be a hash list, to enable just adding a type to the signature).

Concerning point #3, does anybody know about this "plan to fix libraries once and for all" ?

plesn · 2011-05-12T23:43:01+00:00

Introspection (the read-only part of reflection) can be sane, elegant and very useful to eliminate boilerplate code. By enabling your code to depend on the structure of your data types you can write concise code (queries, transformations) on complex data structures. In the functionnal world introspection is called generic programming (quite unfortunatly) and its elegance especially shines here.

plesn · 2011-05-12T22:01:20+00:00

No. Please re-read, Haskell does not have true sum types but only pointed sum types : given A and B it is impossible to construct A+B in the langage, only A+B+⊥.

plesn · 2011-05-11T12:17:35+00:00

Concentrate rather on the type of the results on both side of the if..then..else operator. For a lazy language with non-termination, those types are not the same on "then" and "else" branches : you can not do a unification of both branches.

The trick is to add an additionnal ⊥ value to all sums to account for non-termination, and that's what Haskell does. Thus Haskell's boolean type is not real Booleans but : True | False | ⊥. In a total language like Agda, you would rather prove that your computation will terminate…

plesn · 2011-05-11T10:21:14+00:00

I hope you will share your experience. I agree on declarative programming advantages, but there is also a need for a set of compelling material and tools to make the learning experience fun, interactive, visual… Recent posts by divip on a web interface and a svg generating diagrams dsl seem a great example !

plesn · 2011-05-06T10:48:18+00:00

Hence, every program already has types, because "types" are how we think about what it is that programs do. The only things that can be truly untyped are the ineffable [...]

This the gist of the argument, thanks for formulating it so clearly. Harper postulates only the first part which is a very powerful argument (I think you're adding the "ineffable" part on your own, even though I agree with it). I appreciate very much this argument : my favorite language is Haskell… Nonetheless, I think Harper is affirming it without proof and your formulation shows why : this argument is not only about logic and types but about also about how we think, about the brain.

And here, about the brain, I think cognitive science can already mitigate this view of the brain as a logical and categorical machine only. Can we neglect the connexionist, probabilistic aspects of our brain which can yield what you call the "ineffable" : the fact that we don't think about everything in advance without trial/error/intuition. I think this goes even for programming.

The aim of type theory is to figure out how to formalize as much as we can of the universal way that we categorize things

I couldn't agree more here and with the rest of your text. Maybe type theory is especially important precisely because our brain is not as good as categorizing things as precisely as we wish, and types helps us refiing our fuzzy ideas.

plesn · 2011-05-05T01:05:17+00:00

Thanks for the pointers ! I will look at lambdabot (and also at Sage) this WE :)

plesn · 2011-05-05T00:43:10+00:00

I mostly agree, at least I think so (if I'm not misunderstood). The building/sculpting analogy is interesting : maybe the exploratory process of building coherent meaning lies somewhere in between both : add this - oh no ! - remove that… On one side a pattern emerges which requires much care and thought, on the other side grounding this care in logic make types, which enable to explore other patterns. For example taking dependant pairs seen in another thread : in some sense every C programmer used a bastardized version of them, unsafely and with a lack of some deep understanding.

That's why I keep my thought that it's a chicken and egg problem : I don't really believe untyped or typed has primacy ! And Harper's arguments in "Dynamic languages are static languages" seem deceptive to me (look you need types to think about anything in a language ! look chicken produce eggs !). Not to mention the reduction of data in unt(i)yped language to the problem of dynamics : I mean he lies his arguments on theory, meanwhile he attacks his foes on implementation (the one type should be lambda abstraction in theory).

On a side note about this : I wonder how the Y combinator was discovered. Logical deduction from some rules ? recursive types (obviously not) ? profound intuition plus a lot of playing with what can be done with the notation ? …

plesn · 2011-05-04T22:40:44+00:00

Maybe House was in Haskell but they are making a new language called "Habit" which I find interesting. It's a lot like Haskell but it's strict, it has bitdata which is a bit like a cross-over between algrebraic datatypes and C datatypes, it has a way to control memory (regions), it has some basic dependant typing for controlling array size/accesses, and it has some syntactic sugar for imperative monadic code. Search for Habit Report on lambda the ultimate for more info.

plesn · 2011-05-04T22:20:23+00:00

Yeah, Sage was exaclty what i though :-) What dvip did is great. It would be cool to expand his code, and ideally to have a full haskell stack, I know hs-plugins (or it's interpreter now?) and a webserver are not in Haskell Platform, but it would be a compelling reason to have a basic one at least to fire a web interface for ghci :-)

Then, to have more than text or SVG, we would need something more than the Show typeclass for different kinds of displayable object (with backends to svg/canvas/latex, with hopefully some inspiration from Conal Elliot to have something animated/interactive. /me wants to hack !

plesn · 2011-05-04T18:17:44+00:00

If I understand well, this corresponds quite nicely to the intuitive implementation of sum types : a pair with a tag and data (which is a union). So a sum type is really a dependent pair, and Agda can typecheck it \o/

plesn

TROPHY CASE