pseudonom-

My understanding is that Agda puts much less emphasis on general programming. It's more focused on proving.

Purescript (compiles to JS) also offers Eff: https://github.com/purescript/purescript/wiki/Handling-Nativ....

There's a library at https://hackage.haskell.org/package/probability and a paper explaining the library at http://web.engr.oregonstate.edu/~erwig/papers/PFP_JFP06.pdf.

If revenue from congestion pricing is used for public transit, it tends to be progressive. (Also, those "on the clock" tend to be more sensitive to the high variance caused by congestion.)

I've only messed around in the REPL. https://www.youtube.com/watch?v=lMcRBdSdO_U gives a fairly practical introduction.

There have been deprecation warnings (since 7.8?) about the AMP:

https://wiki.haskell.org/Functor-Applicative-Monad_Proposal#...

There's a list of breakage at:

https://www.fpcomplete.com/blog/2015/03/stackage-ghc-7-10

(I'm not sure what portion of that is due to AMP.)

> Haskell's type system

Shen's type system is probably better described just as expressive.

http://shenlanguage.org/learn-shen/types/types_sequent_calcu... gives a sense of the flavor.

Looking at the studies linked by the article you've linked, their conclusions for high efficacy mostly seem to be of the form "AA increased the likelihood of abstinence". My understanding is that AA, more than other methods, places an emphasis on total abstinence.

It seems that one could support alternative goals (like "reduced incidence of harmful alcohol use") for which AA might not be so well suited.

Your thoughts?

I'm supposing that you meant "includes actual malware". Here's a definition:

Malware, for a given user and computer, is installed software that, in the absence of constraints (such as imperfect information, limited time and ability), would not be installed.

This defines malware as a space rather than a binary, but I'm fine with that.

Though Debian's "popularity contest" is opt-in.

I'm not sure that's a sufficient explanation. Idris and Haskell (with extensions) also have Turing complete type systems. I've never seen either even approach performance like 1 line/minute in real code.

> 1 line/minute

I get that that's an upper limit, but that's still pretty shocking. Is there an overarching reason for this type of performance? Examples of this style of code?

From the linked page:

> Last but not least, Guix is used to build a distribution of the GNU system, with many GNU and non-GNU free software packages. The Guix System Distribution, or GNU GSD, takes advantage of the core properties of Guix at the system level. With GNU GSD, users declare all aspects of the operating system configuration, and Guix takes care of instantiating that configuration in a reproducible, stateless fashion. See GNU Distribution[0].

[0]: https://www.gnu.org/software/guix/manual/guix.html#GNU-Distr...

How does Guix compare to NixOS? Now that both have been around a little while, what are the relative merits of Guile and the Nix expression language, in practice? How big is each community? The Guix package list is much smaller than the NixOS list?

> soy products may cause harmful reductions in testosterone in men. I wouldn't say the data is overwhelming at present, but there is concern.

Not so much. The most comprehensive study of the issue (that I'm aware of):

http://www.ncbi.nlm.nih.gov/pubmed/19524224

Yeah, I didn't mean that as an endorsement of Allwinner. Just a potentially useful piece of information.

> almost certainly due to gluten

Even if you ignore all the messiness of actually existing scientific practice, the math alone doesn't quite say that. It depends on your prior[0] and the power[1] of the study.

[0]: https://en.wikipedia.org/wiki/Bayes'_theorem [1]: https://en.wikipedia.org/wiki/Statistical_power

> It is a fact that they did not work to get mainline Linux support for their SoCs.

Though it is possible. I got mainline Linux running on an A10.

> you'll be stuck with versions of software that are really really out of date

I've had way more trouble with out of date packages on Ubuntu than Debian (Sid).

My understanding is that, after translation, Agda's Haskell makes rather liberal use of unsafeCoerce :: a -> b (it's already been type checked by Agda, after all).

I've heard good things about Certified Programming with Dependent Types (http://adam.chlipala.net/cpdt/).

"This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation."

Edit: There's some comparison of CPDT and SF here: https://lobste.rs/s/c3lj14/certified_programming_with_depend....

> it is seriously behind all of the cutting edge distros that I'm used to.

Are you familiar with branches beyond Stable? I switched from Arch to Debian Unstable (which uses a rolling release) and find their edges to be about equally sharp.

I wonder what makes them say this in the FAQ: "a flexible enough type system for concatenative languages has not yet been designed. However, Factor 2.0 may include optional static typing, if a suitable type system can be found." http://kittenlang.org/ gives the impression of having a fairly sensible static type system.

There are several options for physical units of that sort in Haskell: https://wiki.haskell.org/Physical_units. I remember being fairly satisfied with unittyped: https://bitbucket.org/xnyhps/haskell-unittyped/. Though, enabled by GHC 7.8, units may now be nicer: https://github.com/goldfirere/units

There's also https://github.com/begriffs/heroku-buildpack-ghc.

I've never used Erlang, but Cloud Haskell (http://haskell-distributed.github.io/) and Elm's hot-swapping (http://elm-lang.org/blog/Interactive-Programming.elm) seem to combine an ML-like type system with some of the features you list.

The closest Python analogue is probably named tuples.

It's not exactly what you're asking for but Ur/Web puts an expressive type system to some slightly unusual ends: http://www.impredicative.com/ur/.