more_original

The quality of reviews is a general problem with the reviewing system. Just think about it: You're very busy with other work, you have many reviews to write, about papers that you're not probably really enthusiastic about, and reviews are anonymous to all but the editors. It shouldn't be surprising that this can result in rushed, bad reviews. It's also not too surprising that one can automatically generate a 'review' that looks like someone who forgot about the reviewing deadline and wrote something in a rush.

Nevertheless, while bad reviews do make it through, I do think the editors are able to recognise them for what they are.

I wouldn't be so pessimistic about the possibility to produce useful specifications of real-world systems.

One recent successful large-scale verification is the CompCert C compiler. The compiler is verified relative to a formal specification of a large subset of C. This specification is in the order of <2000 lines of Coq code (see http://gallium.inria.fr/~xleroy/publi/Clight.pdf ). So it is an example of a specification that is much smaller than an implementation and that can be verified manually.

Also, there is good evidence that the specification is correct. From https://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf :

> The striking thing about our CompCert results is that the middle- end bugs we found in all other compilers are absent. As of early 2011, the under-development version of CompCert is the only compiler we have tested for which Csmith cannot find wrong-code errors. This is not for lack of trying: we have devoted about six CPU-years to the task.

This page is 10 years old and is quite outdated.

These days, the official OCaml site is quite good: http://ocaml.org/

These press releases are terrible. It took me quite a while to find the original paper:

Optimizing Indirect Memory References with milk

http://dl.acm.org/citation.cfm?id=2967948

(seems to be available without paywall)

These press releases are terrible. It took me quite a while to find the original paper:

Optimizing Indirect Memory References with milk

http://dl.acm.org/citation.cfm?id=2967948

(seems to be available without paywall)

In 1998 there was one of the strongest El Nino events.

https://en.wikipedia.org/wiki/1997%E2%80%9398_El_Ni%C3%B1o_e...

Maybe this made for a sudden increase, rather than a more gradual one.

No, I do mean formal machines like Turing Machines. Sequential composition of logarithmic space Turing Machines is a standard example for lack of compositionality.

What he means is that complicated programs can be built from simple parts. In programming languages you can just take simple parts and compose them into a single program.

If the simple parts are given by machines, then in general there is no canonical way of composing them into a machine for the composed program. You have to construct a new machine from the machines for the parts. An example is the sequential composition of two functions with logarithmic space usage. You cannot just use run one machine after the other, but you have to modify both machines and then build a new machine that contains them in the right way.

Of course, one may use systematic constructions to combine simple machines into more complicated ones. But this amounts to the implementation of a programming model.

Yes, I know! That's the point I'm trying to make. This whole discussion is about MustardTiger's claim that functors in OCaml have the same meaning as Functor in Haskell. While the latter model functors in the category-theoretic sense, the same cannot be said for the former.

> That is literally the functor.

That would be an answer for Haskell (though a proper one would refer to fmap), but it does not work like that in OCaml. You do know some OCaml, right?

But if it's so obvious, then you can say how it works for the following concrete example:

  module type S = sig
    type t
    val f: t -> int
  end
  
  module F = functor (X: S) -> struct
    type s = X.t * X.t
    let g x = X.f x + X.f x
  end
  
  module A : S = struct
    type t = float
    let f x = int_of_float x
  end
  
  module B : S = struct
    type t = int
    let f x = 2*x
  end
  
  module X = F(A)
  module Y = F(B)

How do I get from X to Y by "literally the functor"?

The point is: In the ML module system there is no equivalent to fmap: (A -> B) -> (F A -> F B), i.e. the functor action on morphisms. So, functors in Haskell and OCaml are different things. If you want to claim otherwise, you'll have to make an actual argument for it.

Ok, so you can't (or don't want to) actually back up your claim that OCaml functors have the same meaning as functors in Haskell. Which is to be expected, because it's bogus. I know OCaml fairly well. The reason you can't show me the map from F(A) to F(B) is that it's not there.

If you want to claim a relation between OCaml functors and category-theoretic functors, then you must be able to justify your claims. Saying "functors represent functions from a module to a module. Oh hey, that sounds just like the standard definition of a functor." is just not a convincing argument.

> Yes there is, the functor.

What we have is a functor F, which would be defined as in:

  module F =
    functor (X: S) -> ....

If you have two modules A and B of signature S, then you can form F(A) and F(B) and these are both modules. Now where are the maps from F(A) to F(B)? Just saying "the functor" does not explain this.

> Just repeating a false statement won't make it come true.

Exactly!

Please read up on the ML module system and its origins.

http://cs.stackexchange.com/questions/9769/what-is-the-relat...

Functors play very different roles in Haskell and OCaml/ML.

In Haskell, the Functor class is there to implement the functoriality of a type. If F is a functor, then one implements maps of type F A -> F B from given A -> B in a functorial way.

In ML, the term functor was chosen because they are not first-class functions, but "a level up" (much like a functor is a level up from the maps in the category that it operates on). However, if F is an ML functor, then there are no "maps" between the modules F(A) and F(B). The morphism part, which is the essence of a Functor in Haskell, is missing in ML. This is why I think that the functor terminology isn't very good in ML.

Not everything that maps one thing to another is a functor.

> >In OCaml, “Functor” is a well-defined term with a completely different meaning

> No, it has the same meaning. It does not behave identically because the languages do not have identical designs.

Functors in Haskell and OCaml are different things. Haskell Functors correspond to the category-theoretic notion of a functor (a thing mapping objects to objects and morphisms to morphisms in a reasonable manner). In OCaml and ML, Functors represent parameterized modules. These are not known to correspond to category-theoretic functors in any reasonable way (and there have been proposals for category-theoretic models of the ML module system). I guess the term Functor is a bit of a misnomer in the ML-like languages.

Incedentally, OCaml gets some of these right.

Record update in constructors is statically checked:

   type myData = MyData1 of { name : string } | MyData2 of { value : int }
   
   let x = MyData1 { name = "hello" }
   (* 
    * rejected:
    * let y = MyData2 { x with value = 0 }
    *)
   let y = match x with
           | MyData1 z -> failwith "todo"
           | MyData2 z -> MyData2 { z with value = 0 }

And one can write:

   match x with
   | A | B -> f1
   | C -> f2

One also finds the terms "formal parameter" (for what is called a "parameter" in the article) and "actual parameter" (for what is called the "argument" in the article).

https://en.wikipedia.org/wiki/Parameter_(computer_programmin...

This reminds me of this culture of cancer cells from a woman who died from cancer in the 50s. The cancer is still alive in laboratories today and there were even proposals to classify it as a new species:

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

Looks like it's currently using the Boehm–Demers–Weiser conservative garbage collector. In scala-native/rtlib/src/main/resources/rt.cpp it includes gc.h and allocates memory using GC_malloc, i.e. not in precise mode.

In 2007 they introduced a unique tax number for every natural person.

In fact, assigning these numbers was complicated by the fact that there is no central registration data base. They started from all the local data bases and then filtered this data to remove duplicates.

Source: https://de.wikipedia.org/wiki/Steuerliche_Identifikationsnum... (sorry, German only)

Here is a source on Wikipedia: https://en.wikipedia.org/wiki/Resident_registration#Germany

"Unlike common belief there is no central administration — except for foreigners (see Central Register of Foreign Nationals (Germany)) — the resident registration is run by 5283 local offices throughout Germany."

For passports, I'd guess that there is a different database.

Interesting. In Germany this database does not even exist. Each town keeps its own data and they are not connected. I think the reason for this are the evil uses of data bases by the Gestapo during Nazi times.

> 2. start gaining momentum (e.g. why should I use Linux, when on Windows I can run both Linux and Windows applications)

Remember OS/2 2.x? It could run Windows 3.x binaries, including GUI programs. The result was that noone wrote programs for OS/2. Windows programs would run both on Windows and on OS/2, so why write another one for OS/2?

Why should anyone port Linux programs to Windows now? Just write for Linux and it will work both on Windows and on Linux. So now you actually have more reason to target Linux.

How do you read "The computer itself was developed at a research institute outside Moscow" to mean anything other than that the computer was developed in Russia?

This is the first I hear about the Robotron 1715 being developed in Russia. All other sources I can find say that it was developed and built in Eastern Germany (Robotron was an Eastern German company that developed a number of computers in the 80s). Even the russian wikipedia say so. Wikipedia says that even the U880 processor, a Z80 clone, was produced in East Germany.

https://ru.wikipedia.org/wiki/Robotron_1715

http://www.old-computers.com/MUSEUM/computer.asp?c=864&amp;s...

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

Perl's regex engine must use something stronger than plain NFAs. The expressive power of NFAs and DFAs is exactly the same. They both recognize the regular languages, which is less than what can be expressed with Perl "regular expressions".

In Germany it's mandatory for children to ride on the sidewalk. But for an adult accompanying the child, it is illegal to ride on the sidewalk.

One technical reason that makes me prefer OCaml to Haskell is Haskell's weak module system. I think there should be a good way to parameterize one module over another module (interface) and to use different instantiations of the module in the same program. I think people do such things using type classes and typing constraints. But I found this being awkward, because the compiler needs to be able to resolve the constraints automatically and there are issues with overlapping instances and the like.

To quote Bob Harper: As a consequence, using type classes is, in Greg Morrisett’s term, like steering the Queen Mary: you have to get this hulking mass pointed in the right direction so that the inference mechanism resolves things the way you want it to. [https://existentialtype.wordpress.com/2011/04/16/modules-mat...] (I think this applies most of all if one is using type classes to emulate a module system. For other purposes, type classes are quite nice.)

Maybe Backpack will solve these issues. [http://plv.mpi-sws.org/backpack/]

Yes, because I really didn't want an FB account (closed it since). There were even doubts about the legality of Spotify requiring an FB account in Germany: http://www.noz.de/artikel/61551360/datenschuetzer-kritisiere...

It used to require a facebook account initially (at least here in Germany, right after the launch). I had to create a one in order to open a Spotify account. The option to register using an e-mail address was added later and I migrated my account when this was done.

For cycling in an area one doesn't know, the Strava heatmap is also quite useful. It shows the routes that other cyclists take and can be helpful in finding good cycleable routes.

http://labs.strava.com/heatmap