mrkgnao

Trifecta has poor documentation. I've been thinking about reading the Idris parser to learn trifecta/parsers.

Blogger is actively hostile to phone browsers. For horizontal scrolling, you can try dragging at an angle (to fool the page-change JS) and then vertically scrolling to negate the vertical component of the first motion. It becomes pretty natural after a while :/

What made me move back to Google from DDG is the (by construction?) inability of the latter to learn what you're interested in. For things like documentation search, Google quickly starts tailoring results to $LANG.

Yes! More "real-world" Haskell is always good. This seems like a good time to bring up Shake, Neil Mitchell's build system:

http://shakebuild.com/

It can be used like CMake (as a build script generator) or like Ninja. For many projects (including building Ninja), it's faster than Ninja. Chromium is a notable exception: it has a huge set of Ninja files, and the Shake parser is not as fast as Ninja's parser.

From the docs:

> [...] compiling LLVM on Windows under mingw they both take the same time to compile initially, and Ninja takes 0.9s for a nothing to do build vs Shake at 0.8s. Shake is slower at parsing Ninja files, so if you have huge .ninja files (e.g. Chromium) Shake will probably be slower. Shake does less work if you don't specify deps, which is probably why it is faster on LLVM (but you should specify deps -- it makes both Shake and Ninja faster). As people report more results I am sure both Shake and Ninja will be optimised.

https://github.com/ndmitchell/shake/blob/master/docs/Ninja.m...

A Summer of Haskell project is on to migrate GHC to a Shake-based build system.

PS. Wow, Annie Cherkaev's website looks really different now.

> conspiracy theories around popcount and the NSA

Whoa. Some links (with sometimes not-very-well-thought-out allegations):

https://groups.google.com/forum/#!topic/comp.arch/UXEi7G6WHu...

https://www.schneier.com/blog/archives/2014/05/the_nsa_is_no...

Haskell can, in fact, express the CardValue example using DataKinds. (I haven't written it out, though.)

Would that be related to an existential type of the form

    foo :: a -> (forall b. Show b => b)

from Haskell?

They are much closer to the curves and solids we're familiar with from everyday experience. For example: you have well-defined tangents at every point for a smooth curve, but a self-intersecting curve doesn't. So many techniques and a lot of intuition carries over into the abstract algebraic setting.

More generally, algebraic geometry is a central field of math because it is, basically, about solving polynomial equations. It's one of the most "well-connected" fields of mathematics today. Number theory, differential geometry, complex geometry, even differential equations: all these fields benefit from their interactions with modern algebraic geometry. (Also biology, I've heard. Lior Pachter is a name I remember in this connection.)

I made a top-level parent comment about a result from March 2017. Otherwise, things that either will become part of history, or suggest directions for work that will:

* Green-Tao theorem, and lots of other work involving Terry Tao

* Yitang Zhang's work on prime gaps, and subsequent improvements

* Bhargava and collaborators' work on elliptic curves

* The introduction of algebraic topology methods into algebraic geometry (aka "simplicial"/"derived" stuff, see Jacob Lurie)

* Homotopy type theory

* Mochizuki/ABC stuff

* Peter Scholze's work in arithmetic geometry

As I understand it, a significant portion of the cleverness is in the audacity of encoding something liar paradox-like into a formal logical framework (and perhaps also the precision with which logics were specified and differentiated from one another).

Well, a couple decades later we have the era-defining unification of geometry, algebra, and number theory building on the work of Noether, Hilbert, Weil, and so on.

To drop a few names, we had Grothendieck, Serre, Deligne, Wiles, Illusie, (the elder) Artin ... and it's continued to this day. Wiles' proof of FLT built upon this beautiful synthesis of ideas, for example.

> 1964

> Hironaka solves a major problem concerning the resolution of singularities on an algebraic variety.

Essentially, sometimes the varieties (which are geometric objects like curves, surfaces, etc.) studied in algebraic geometry are singular: they might have singularities, like nasty self-crossings or sharp edges. Hironaka's result lets you take a "bad" variety and "resolve its singularities", giving you a good (nonsingular) variety which you can work with instead.

This is in "characteristic zero", i.e. over fields like the real or complex numbers. We also have fields of positive characteristic, e.g. the integers modulo any prime number. Over such fields, I understand that this is a much harder problem to solve.

The aforesaid Heisuke Hironaka is 86 now.

In March of this year, he published a (purported) proof of resolution of singularities in positive characteristic.

The /r/math thread has some good explanations.

https://www.reddit.com/r/math/comments/6aqwbo/hironaka_publi...

For some reason this reminds me of how hard it is to design unsupervised learning systems that don't hit a measurable payoff for a long time, so they can't easily decide what they did right or wrong.

Also, I love your username :)

> popularizing only applied mathematics is betraying pure mathematics

I'd say it's betraying mathematics.

Someone hacked together something very similar with Haskell arrows.

http://scrambledeggsontoast.github.io/2014/09/28/needle-anno...

Last time this happened I had to write a couple whole walls of text. There's more to this than you think! :)

https://news.ycombinator.com/item?id=14016396

Oh, this is interesting!

http://www.cprogramming.com/tutorial/template_specialization...

What you have towards the end of that post is actually something like

  type family Vector a where
    type instance Vector (Ptr a) = ...
    type instance Vector a = ...

This is a closed type family. (Think of it as a pattern-match on types where the cases are tried in order.) Very cool!

I still don't know how the linear algebra/Eigen examples might work, though.

This post has a good overview of what can be gained by the use of these techniques:

http://www.randomhacks.net/2007/02/10/map-fusion-and-haskell...

> Using just these two rules, I saw a 225% increase in the number of nodes processed per second. Under the right circumstances, GHC can even outperform C code by applying these kinds of inter-procedural optimizations.

Also, we have QuickCheck, which allows us to check properties by randomly generating testcases. The post I linked mentions this.

I've heard a little about generics/templating/whatever-you-call-the-things-between-angle-brackets techniques in C++ from far away.

> The specialization example is the same as template specialization in C++.

This sounds very interesting to me, because you're saying it's accomplished entirely in the type system: do you have an example or a reference you can point me to?

I'm guessing there's a type-level tag for an algorithm, and the compiler is told how to combine tags corresponding to a sequence of operations on vectors that looks a certain way. Something like do_the_thing<t, DotWith<Self>, HasFastNorm<t>> = do_the_thing<Norm<t>>? (just thinking aloud in pseudo-C++, nothing to see here, move along) In that case, it would be closer to something using a function on types, which Haskell has in the form of type families.

You're right, of course. There are ways around this: for one, without optimization (i.e. -O0) you don't have any rewrite rules firing, so any discrepancies in behavior can be tracked down this way.

In practice, most of the libraries that include tons of rewrite/specialise/inline (ab)use are either "core" libraries (like vector/bytestring) or have a large userbase (e.g. Conduit), and rules don't really change too much from version to version, so this has never actually had the detrimental effects that "silent replacement of code" might have in the worst case.

This might[0] sound similar to apologetics for dynamically-typed languages: the only real answer to your question is that rewrite rules are ultimately a way to improve performance, and they come with caveats usually associated with replacing clearer algorithms with faster ones. (I'm thinking of the adaptive sort from the C++ STL, which iirc uses different sorting algorithms for differently-sized containers to maximize expected performance. It's not exactly intuitive that vectors of size 100 and vectors of size ~10000 are sorted differently, is it?)

Of course, the only verifiably-correct way to do these things is through the use of machine-checkable proofs of the transforms. The well-known "foldr/build" rule that many optimizations of linked-list functions reduce to, for instance, has been proven outside of GHC, and there are usually similar proofs for other rules known to the library author. The appeal of dependently-typed languages is how they are a nice vehicle for the inclusion of those proofs in library code: if the compiler can't verify that your rule makes sense, it can complain instead. You then end up supplying a proof, or saying "just believe me, okay?" ;)

[0]: "In practice"? Seriously? Next thing I know I'll be parroting "in the real world" and so on...

Yup. A good one isn't enough, though, it's the constant evolution that's awesome: type/data families are pretty new.

In Haskell your example would look like

  x = do
    ints <- grabSomeIntegers
    return (ints & map (*2) & filter (> 3) & map (-1))

(where x & f = f x) which the compiler desugars into something like

  x =  fmap (map (- 1) . filter (> 3) . map (* 2)) grabSomeIntegers

Now the compiler can very well perform optimizations on the big composed function. Even then, as you say, this has its limits: polymorphic/DRY code still suffers a performance penalty because it has to work the same way with all allowed inputs.

... right? Nope, that doesn't have to be the case: Haskell supports more than just your $grandparent's parameterized types!

The vector package uses something called data families to have different in-memory representations for vectors of different types, without "letting go of the DRY" at all.

https://www.stackage.org/haddock/lts-8.15/vector-0.11.0.0/sr...

Here, Vector a is a data family: how a value of type Vector a "looks" in memory depends on a. So you'll notice a bunch of lines of the form

  newtype instance Vector Int16 = MV_Int16 (P.Vector Int16)

What this means is "if we have a vector of values of type Int16, use a primitive vector (essentially a raw array) to represent it in memory". (P is an alias for the Data.Vector.Primitive module.) Now I can write code that uses the beautiful user-facing API of vector:

https://www.stackage.org/haddock/lts-8.16/vector-0.11.0.0/Da...

Written using vectors, code like in your example is perfectly DRY; it would look like (this is untested code!) this:

  combobulate :: Num a => IO (Vector a) -> IO (Vector a)
  combobulate = do
    as <- grabSomeIntegersFromNetwork
    return (ints & V.map (*2) & V.filter (> 3) & V.map (-1))

and under the hood, whenever I use a Vector Animal[0], it uses whatever fast general-purpose array implementation is available, but the moment I call this with a vector of Int16 or Bool or Complex Double, it switches to the fast implementations in the Primitive/Internal modules.

The key is the data families: the types expose a simple, consistent API, hiding the actual guts of the memory representation from the user. The library author is free to perform whatever ugly/evil/unsafe manipulations she feels like behind the scenes on the internal representations, or not.

[0] Defining numeric operations on animals is left as an exercise to the careful reader.

I'm posting this as a top-level comment, but it's really a reply to the discussion downthread about compilers being able to work magic if we let them. Better still, why not help them?

Something I took for granted for the longest time about Haskell (which remains the only language I know of with the feature) is the ability to write user-defined "rewrite rules". You can say, "okay, GHC, I know for a fact that if I use these functions in such-and-such way, you can replace it by this instead".

  {-# RULES 
    foo x (bar x) =  
    superOptimizedFooBar x 
   #-}

A rule like this would be based on the programmer's knowledge of FooBar theory, which tells her that such an equality holds. The compiler hasn't studied lax monoidal FooBaroids and cannot be expected to infer this on its own. :)

Now, anywhere a user of this code writes something like

  foo [1,2,3] (bar [1,2,3])

the compiler will substitute

  superOptimizedFooBar [1,2,3]

in its place. This is a nice way to bring the compiler "closer" to the programmer, and allow the library author to integrate domain-specific knowledge into the compiler's optimizations.

You can also "specialize" by using faster implementations in certain cases. For example,

  timesFour :: Num a => a -> a
  timesFour = a + a + a + a

  timesFourInt :: Int -> Int
  timesFourInt x 
    = rightShift x 2

  {-# RULES
      timesFour :: Int -> Int
    = timesFourInt
   #-}

If you call timesFour on a double, it will use addition (ha!) but using it on an Int uses bitshifting instead because this rule fires.

High-performance Haskell libraries like vector, bytestring, text, pipes, or conduit capitalize on this feature, among other techniques. When compiling code written using libraries like this, this is how it goes:

- rule #1 fires somewhere - it rewrites the code into something that matches rule #2, "clearing the way" for it to fire - rule #2 fires - rule #3 fires - rule #1 fires again - rule #4 fires

and so on, triggering a "cascade" of optimizations.

The promise of Haskell is that we already have a "sufficiently smart compiler": today, with good libraries, GHC is capable of turning clear, high-level, reusable functional code with chains of function compositions and folds and so on into tight, fast loops.

--

I must add, though, that getting rewrite rules to fire in cascades to get "mad gainz" requires one to grok how the GHC inliner/specializer works.

http://mpickering.github.io/posts/2017-03-20-inlining-and-sp...

Data.Vector also utilizes an internal representation that makes fusion explicit and hence predictable (inevitable, even) called a "bundle":

https://www.stackage.org/haddock/lts-8.16/vector-0.11.0.0/Da...

but this relies on rewrite rules too, e.g. the previous module contains this rule:

  {-# RULES

  "zipWithM xs xs [Vector.Stream]" forall f xs.
    zipWithM f xs xs = mapM (\x -> f x x) xs   #-}

This might end up being the Rust "killer app"! (Servo aside, of course.)

There's a Summer of Haskell project going this year. I think it's called WebGHC?

Edit: https://webghc.github.io

Emacs' evil-mode provides "live" search-and-replace. I can't imagine using the vanilla Vim behavior any more.

Nah, you haven't really avoided success at all costs until you've evangelized a committee-designed functional language with pervasive laziness.

Thank you for the link to that book.

I sometimes ponder, against my own experience from experiencing the mathematical side of things, how the "folklore" wisdom in the medical community is almost certainly something that the rest of us might benefit from (this probably started when I read The Emperor of All Maladies a couple years back) considering the issues that the mental part of it deals with: ethics, conduct in a power-unequal relationship, consent, the moral imperative to evaluate risk competently (and the recognition that the former can never be done perfectly), telling the truth and intention/effect differences ("you're almost certainly going to die"/"this is a miracle!"), not to mention the elephant-in-the-room question of living with death as a close acquaintance and learning not to become consumed with either anger or despair at what one considers personal failings.

(I suppose the late Oliver Sacks's work is an instance of what I'm talking about.)

I understand that traits are something like typeclasses or interfaces: are single-method traits kept around as traits, or is the function itself passed around in the optimized output?

I'm actually suddenly curious about how other functional language compilers look compared to GHC.

I wonder, does #(* %1) do anything sensible?