YorkshireSeason

41 ms·

331.
by YorkshireSeason 9y ago
> does not correspond to what derived implicits do I did not claim it did. The first example disproved ionforce's claim that default values cannot be constructed dynamically. > Define `a` as `y` to shadow the function parameter,
332.
by YorkshireSeason 9y ago
I've moved to Scala in 2012 (because I needed to work on the JVM) from over a decade of Ocaml. I found that the absence of full type inference was not a major problem. The JVM library ecosystem on the other hand ... lack of libraries (
333.
by YorkshireSeason 9y ago
I'm not saying implicits and default parameters are the same thing. I'm saying the key idea behind implicits is the realisation that default arguments merge two ideas that should be kept separate, if we want context dependent defa
334.
by YorkshireSeason 9y ago
> injecting values constructed dynamically You can also do this with default arguments, e.g. like so: let f x y = let g (a = x+1) b = ... ... For example the following is valid OCaml: let bump ?(step = 1) x =
335.
by YorkshireSeason 9y ago
> Akka loves the things. So? Treat Akka as a black box. You can always explicitly pass implicit arguments.
336.
by YorkshireSeason 9y ago
What is your main complaint with implicits? If you don't like them, why don't you add "Use of implicits forbidden" to your coding style guidelines, and check in code-reviews, and add a "grep implicit" check to
337.
by YorkshireSeason 9y ago
> Have you spent any time at all using them? Sure I have used both. Default arguments and implicits both have the same key idea: you can omit arguments to functions, and the compiler, guided by type information, synthesises the missing a
338.
by YorkshireSeason 9y ago
From an abstract PL theory POV, Haskell's key innovation over ML was HKTs. It was an experiment at the time, but one that was successful beyond all expectation: I cannot imagine designing a new PL without HKTs. (Note that Rust is also
339.
by YorkshireSeason 9y ago
Haskell is category theory as a language. I disagree with this. Haskell's creation [1, 2] predates the realisation (by the FP community at large) of the close connection between parts of category theory and parts of pure f
340.
by YorkshireSeason 9y ago
Marx and Engels most certainly did not think equality of outcome was a cornerstone of communism, on the contrary. Just think about "From each according to his ability, to each according to his needs" from Marx Critique of the G
341.
by YorkshireSeason 9y ago
Fringe is clearly a vague predicate. One way of defining Fringe is via the number of followers that can be mobilised for political action. E.g. in the UK the Tories , and Labour are not fringe, but CISTA (Cannabis Is Safer Than Alcoho
342.
by YorkshireSeason 9y ago
The anarchists, qua bombings, played a potent role in 19th, and early 20th century politics, but not a good one. Politically, anarchists are really quite different from the socialist/communist tradition: - Anarchists: reject the state
343.
by YorkshireSeason 9y ago
I invite you to defend your claim. Start by asking yourself which non-fringe socialist/communist party was not using the Leninist model of organisation, and which was not a member of the ComIntern and its successors? Which did not rece
344.
by YorkshireSeason 9y ago
Railing against "the state" or "our corporate overlords" is not a mature political position, but merely unfocussed, reflection-free rage that gets tooled / channeled by political organisers and activists on the lef
345.
by YorkshireSeason 9y ago
I was clearly referring to 46886532558's "reeeally left wing", i.e. extreme left. It is historically accurate to identify the extreme left with the ComIntern, i.e. the Soviet communist party, ruled during his lifetime by S
346.
by YorkshireSeason 9y ago
I have commented not on the CCC but on user: 46886532558's original claim that being "reeeally left wing" is somehow a plausible reason for being anti-surveillance. This association is misleading, and I feel a responsibility
347.
by YorkshireSeason 9y ago
they are like reeeally left wing The historical record of the extreme left is extremely pro-state, pro surveillance. Indeed, the Marxist corrective to freewheeling capitalism was a strong socialist state (to cover the period befo
348.
by YorkshireSeason 9y ago
what they get out of it My interpretation is that the ROC sees this as a bargaining chip, to be given up in exchange for something else, at an opportune moment. The ROC doesn't have much else to offer to the mainland at the mo
349.
by YorkshireSeason 9y ago
Meyer had a clearcut idea what he wanted from tooling. And that has not yet been achieved, neither by him, nor by anybody else. Maybe this will change in the future.
350.
by YorkshireSeason 9y ago
Most PLs don't take off. Language choice is mostly dependent of social factors that can be summarised as "network effect". In PLs that manifests itself primarily through a lack of mature and numerous libraries. Eiffel had add
351.
by YorkshireSeason 9y ago
Why do you say "hello, nice to meet you"? I imagine that this document was written to a target audience, propbably so as to satify some funder's requirement, e.g. as 'post-mortem' for his ERC grants. Audiences have
352.
by YorkshireSeason 9y ago
Meyer's most interesting sentence is the last [1], about the extent to which he achieved his research goals at ETHZ: [T]he story told in this article is one of glaring, unremitted and probably definitive failure. What
353.
by YorkshireSeason 11y ago
Sure, and dismissed it. Not all cultures, not all parenting styles, are alike and produce the same outcomes. Some cultures have more affinity towards academic achievement than others.
354.
by YorkshireSeason 11y ago
This discussion goes way beyond an "absolute layman explanation to homotopy type theory" ... Anyway, I disagree that the "whole idea of type theory is that things can have more than one proof". UIP is about identity typ
355.
by YorkshireSeason 11y ago
Exactly. Here is an implementation of Cantor's diagonal method in Agda which is entirely constructive: http://www.playingwithpointers.com/agda-cantor.html
356.
by YorkshireSeason 11y ago
It is wrong to say that it's key novelty is that "Homotopy type theory: extends type theory with proofs of equality in a proper way". This was done already with Martin Lof's type theory, as used in e.g. Agda. Homotopy t
357.
by YorkshireSeason 11y ago
What is the state of the art of the research on the computational interpretation of univalence? What's working, what's not working? I seem to remember that A Jeffrey said not too long ago that he had a working interpretation.