mrkgnao

In Haskell:

    fac :: Int -> Int
    fac x = case x of
      0 -> 1
      n -> n * fac (n-1)

or even

    {-# LANGUAGE LambdaCase #-}

    fac :: Int -> Int
    fac = \case
      0 -> 1
      n -> n * fac (n-1)

The goal of Principia Mathematica was not "to prove that 1+1=2". It was meant to be a new set (ha!) of foundations for mathematics.

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

Some extensions are considered bad ideas later, e.g. -XImplicitParams.

Some extensions can make existing code fail to compile, e.g. -XOverloadedStrings.

Some extensions are fairly specialised and their use can cause error messages that are confusing if you don't know what the extension does, e.g. -XAllowAmbiguousTypes.

Some extensions can cause certain pathological pieces of code to suddenly start behaving weirdly, e.g. if you turn on -XApplicativeDo for a type whose Applicative instance isn't lawful, but whose Monad instance is.

Of course, many, many extensions could be enabled by default without making the UX worse or restricting the set of allowed programs at all: a large section of Haskell users is likely in favour of enabling syntactic conveniences like LambdaCase or MultiWayIf, or automatic code-generation utilities like DeriveFoldable, DeriveTraversable, and so on. That's what Haskell Prime is for, I suppose.

Why was there such a spike in Haskell searches in August 2015?

https://trends.google.com/trends/explore?date=today%205-y&q=...

> Linux is licensed under GPL, so the best improvements end up in the main tree

Without taking sides in the debate, grsecurity/PaX patches are a counterexample.

A (not necessarily original) example would be nice.

> Compiler would infer the types, and the programmer would read it and say, oh, I agree with this type, but I disagree with this type, that's perhaps wrong, this should be rather that type. Then the compiler would infer types again, based on programmer's incremental input.

This is possible today, at least in Haskell. (and I'd guess in OCaml too ... surely also Scala?)

Your proposal for adaptive data structure selection based on benchmarking is intriguing!

Does Guile (or even Chicken) do anything similar?

(My only exposure to it is from Andy Wingo's blog, and I don't know much about Scheme.)

MagicHaskeller[0] (which seems to sadly be offline at present) is a similar project that infers Haskell functions from properties like

   reverse "abcde" = "edcba"

Other, older projects include Exference[1] and Djinn[2], in decreasing order of power.

Also, this is really similar to how Idris and Agda work, except they use expressive types to generate the code (using the Emacs modes) rather than test cases.

[0]: http://nautilus.cs.miyazaki-u.ac.jp/cgi-bin/MagicHaskeller.c...

[1]: https://github.com/lspitzner/exference/

[2]: http://www.hedonisticlearning.com/djinn/

The response to the recent Rich Hickey talk definitely points toward "dynamic typing as its own solution" (instead of a stop-gap until someone makes static typing less "verbose") being a popular view nowadays.

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

Haskell lends itself pretty well to "backend"[0] work, and there are more than a few organisations using it to write servers, trading systems, and so on. It definitely fits his metric, which is "> 1000 industrial users".

[0] (Unlike applying it to the frontend, which is a comparatively less mature situation with multiple proposed solutions.)

> What you get "for free" from such languages may not be significant enough to justify the cost of adoption

Idris can often infer entire functions from their types if the domain is amenable to accurate type-based specification. For instance, taking the common "sized vector" example, where `Vec n a` refers to a length-n vector of values of type a, functions like

    zip : Vec n a -> Vec n b -> Vec n (a, b)

can be automatically generated via the interactive "proof search" mechanism that the Emacs integration for Idris provides. Similar things are possible in Agda, which is however squarely aimed away from the "practical use" market.

Sometimes people even write a systemd unit for it. Feature, not a bug, etc.

Essentially, Nix treats every version of a package, or every "instance" of a package compiled with different flags, or different "build inputs", as a completely different dependency. So foo-1.0, foo-2.0, and foo-2.0-debug are all separate things you can depend on, from the POV of the package manager. A huge "symphony" (a friend's term) of symlinks holds it all together.

I can get it down to 1ms, so there's probably something wrong with my setup. (I just look for how the cursor moves; on the delayed one, I can discern the presence of the cursor on the next line for a split second.) Maybe monitor refresh rate, or the minimal resolution sleep can handle?

I'm using Alacritty, which is supposed to be really fast and everything!

Um, just to be clear: can I write a program that depends on both A and B? Nix lets you do that.

I used Arch Linux for a while (~3 years) before making the jump to NixOS.

Many things I got from AUR packages are binary-cached in stable Nixpkgs, not to mention "compilers" (GCC, clang, and various versions of GHC in my case). I don't know when you last tried it out, but binary availability isn't a problem now if you'd like to give NixOS a spin. The only thing I build from source is polybar[0].

[0]: https://github.com/jaagr/polybar

I believe GP was asking if you could have packages A and B installed simultaneously if

  - A depended on version X of C
  - B depended on version Y of C 
  - X != Y

I looked a few things up after Michael's post, and it seems there are a lot of resources and codified idioms around writing chess engines in C. (E.g. tons of bit-twiddling hacks, many related to the fortuitous existence of 64-bit integers. [Not that you can't do those in Haskell.])

NurdRage, a relatively popular YouTuber, also replicated the Epipencil experiment on his channel.

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

The reason I'm bringing him up is that he synthesised Daraprim (pyrimethamine) from domestically-available materials over a period of ~2 years.

https://www.youtube.com/watch?v=ddCuWX4vtOA&list=PLU79801KtV...

There's an NMR spectrum at about 12:08 in the last video in the playlist, which shows that he doesn't quite have medical-grade Daraprim, and that he'd need a lot of purification to get there.

I'm not sure whether I agree or disagree, but I'm reminded of how it's said that Fermat's Last Theorem wasn't really the goal (or even that the truth or falsity of FLT doesn't imply anything interesting on its own), but it's an extremely vital problem from a development-of-math perspective.

Ideals were discovered by Dedekind as a solution to an error made by Gabriel Lamé in his claimed proof of Fermat's Last Theorem: he'd overlooked that not all rings have the same properties as Z. In this situation, they were missing "unique factorization", which Kummer "fixed" by hypothesizing the existence of "ideal numbers", which Dedekind later formalized as "ideals". This was a huge step forward for the development of modern algebra.

https://www.quantamagazine.org/the-crazy-number-that-almost-...

And that's setting aside a lot of algebraic number theory, class field theory, and so on.

The closest thing number theory has to a Grand Unified Theory is the Langlands program. It's a huge, highly interconnected, often surprising bunch of conjectures relating number theory to geometry, algebra, and even[s] string theory -- and also something that I know next to nothing about. :)

I'll put the Wikipedia[w] intro here, and note with some happiness that Frenkel has used that exact phrase before:

> In mathematics, the Langlands program is a web of far-reaching and influential conjectures about connections between number theory and geometry. Proposed by Robert Langlands (1967, 1970), it seeks to relate Galois groups in algebraic number theory to automorphic forms and representation theory of algebraic groups over local fields and adeles. Widely seen as the single biggest projects in modern mathematics, Edward Frenkel described the Langlands program as “a kind of grand unified theory of mathematics.

Wiles' proof of the modularity theorem (and hence Fermat's Last Theorem) is a proof of a some of the Langlands conjectures "in dimension 2": one of the pinnacles of human mathematical achievement is just an incomplete portion of a special case of Langlands' vision.

> Andrew Wiles' proof of modularity of semi-stable elliptic curves over rationals can be viewed as an instance of the Langlands reciprocity conjecture, since the main idea is to relate the Galois representations arising from elliptic curves to modular forms. Although Wiles' results have been substantially generalized, in many different directions, the full Langlands conjecture for GL(2, Q) remains unproved.

To give you a little taste, here's a 10000-miles-above-the-ground view of what this says.

A modular function is a certain kind of object in complex analysis (something like calculus with complex instead of real numbers[c]).

A Galois representation starts with a Galois group, which tells us something about the large-scale structure of a number system, and extracts[p] ("represents") a small part of the information it contains: the full "absolute" Galois group is incomprehensibly complicated. Every elliptic curve gives rise to these representations.

There's no reason these things should be related: most number thought the modularity conjecture was an improbable goal. Now think about how it's just a tiny part of a much larger whole. They don't call it "fantastically bold"[n] for nothing.

---

[w]: https://en.wikipedia.org/wiki/Langlands_program

[s]: https://physics.stackexchange.com/questions/4748/why-is-ther...

[n]: https://golem.ph.utexas.edu/category/2010/08/what_is_the_lan...

[p]: As I understand it, Wiles' proof only uses 2-dimensional representations.

[c]: ... but it's hard to overstate how much nicer and more uniform everything becomes!

This sentence doesn't really make sense, insofar as TFA isn't about some conjecture.

Optionals are also "applicative", but Haskellers used them for a long time before applicative functors became popular. A concept can support a certain way of thinking about it without everyone needing to think that way :)

Working with streams of data often makes pointfree syntax beneficial, since you can start to see the omitted arguments "flow" through your chain of composed functions. If you write

   f # g = \x -> g (f x)

then you could implement functions like this:

   f :: Stream Int -> Stream Int
   f = drop 3       -- drop the first three elements
     # skipEvery 3  -- skip every third element
     # sumEvery 2   -- sum every consecutive pair of elements
     # map (* 2)    -- double everything

This would turn

   1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, ...

into

   2 * (4 + 5), 2 * (7 + 8), 2 * (10 + 11), ...

You can find many non-pointfree versions of similar streaming code here: https://github.com/snoyberg/conduit/

Thanks! I'd say at least some of the blame for that is due to how C-family languages make these concepts appear somewhat ... opaque.

I won't comment on Haskell's speed here, but function composition can't possibly be making Haskell less faster.

The reason is simple: the compiler inlines the composition operator in the vast majority of (probably all?) cases, since the Haskell standard library source code marks it with an INLINE pragma:

   -- | Function composition.
   {-# INLINE (.) #-}
   (.)    :: (b -> c) -> (a -> b) -> a -> c
   (.) f g = \x -> f (g x)

http://hackage.haskell.org/package/base-4.10.0.0/docs/src/GH....

Tasteful, minimal pointfree-ization can sometimes help one think at the "level" of functions instead of thinking about how those functions transform arguments.

If you're familiar with the Maybe type (called Option in Rust and Java, and perhaps Swift?), this example might help. For concreteness, this is how it's defined in Haskell:

   data Maybe a = Nothing | Just a

Consider this function, called `maybe` in Haskell:

   maybe :: t -> (a -> t) -> Maybe a -> t
   maybe defaultVal _ Nothing  = defaultVal
   maybe _          f (Just v) = f v

This unwraps a Maybe value, transforming the value inside if it exists and taking a default to return if it doesn't. So, for example

   > maybe 4.0 sqrt (Just 9.0)
   3.0

   > maybe 4.0 sqrt Nothing
   4.0

Now consider this function:

   withMinDefault :: Maybe Int -> Int
   withMinDefault =  maybe intMin (* 2)

Here (* 2) is a partially-applied function that doubles a number: ((* 2) 3) = 6. The advantage of defining `withMinDefault` like this instead of the equivalent "pointful" version

   withMinDefault' :: Maybe Int -> Int
   withMinDefault' n =  maybe intMin (* 2) n

is minimal at best, but the idea is that we're defining this function in terms of `maybe` directly:

   "withMinDefault multiplies an optional number by 2, 
   defaulting to INT_MIN if it's not present."

You can combine this with function composition to start working by almost exclusively manipulating functions, and (when done tastefully, as I stated at the beginning) it can greatly improve the clarity of the code for an experienced programmer who can read streams of functions with facility.

When you forgot $EDITOR, ^O^X had your back. :)

Using even better (PureScript) syntax, the pointfree version of the latter can be written in notation similar to a hom-functor.

   f1 = pow 2
   f2 = pow _ 2

This makes it look like a lambda but without having to bind an argument explicitly. Makes it much nicer to write complicated expressions (although I can't speak to the readability for people less fluent in the syntax).