icen

Yes, `%` is division. It's not that odd, if you look at the symbol - it looks quite similar to the division symbol `÷`.

It's almost better asking where C got the idea that it should be mod from!

But how many of them come from the rendering engine?

There's always the `unsafe` escape hatch - if you need to potentially alias mutable pointers, you can (via using the 'raw pointer' types `const T` and `mut T`).

You can only do this in an `unsafe` block. If you get a bug caused by aliased mutation, then you know exactly where it comes from.

For good reason! This is Rice's theorem.

Such a structure is called a Zipper, for anyone wanting to look into it further.

The &* thing is due to Deref coercions. The deference operator is a trait (Deref), which has an associated type that it dereferences to. This lets you do nice things, like dereference a Box<T> to just a T, and let the Box implementation figure out how to get you there. (It's also used on method calls using .)

What you have is a reference to a type with a Deref-coercion to the type you want, but the compiler won't coerce under the reference for you, so you have to dereference and then reference it again, and then type inference can work out that you wanted to reference the coerced type.

Conflating these seems a bit disingenuous. It seems plausible that you can innately know your sex, and that this comes with some behaviour. It's not the same as saying that girls being associated with the colour pink isn't a social construct.

Introduction to category theory via haskell, and not learning the right areas of abstract algebra?

It's plausible to even do a degree in mathematics and never encounter the name 'monoid' - you'll obviously encounter the structure, but my abstract algebra classes just skipped ahead to groups, and then to rings and modules, instead of spending any time on the simpler structures.

Other times, like when studying formal languages, because regular languages are a monoid, the structure is introduced, via noting that you have an empty language and a method to combine any two languages, but not given the name monoid.

So you come across haskell, and it gives a name to things like monoids, monads, functors, and so on, and says that monads and functors come from category theory, and it seems like a valid inference to say that monoids also come from category theory.

The author has a bunch of similarly named projects (Morte, Annah).

evil-mode

You should check out magit, as well.

As in, it is still 20 years ahead of its time, or was it's moment somewhere in the 80s?

The 'abusiveness' is the use of `>>=` as a constructor, instead of its more standard role as member of an interface.

The author is using it to take advantage of syntactic sugar that is now reliant only on names and types, instead of implementation of the relevant interface.

A similar idea is to use `::` and `Nil` as constructors, which let you use the `[a, b, c]` list syntax (desugared to `a :: b :: c :: Nil`) for things that aren't actually lists. It can be convenient, but can also result in confusion.

And this is the case in Idris, where `cast` is a member of the `Cast` interface, and there's an implementation of `Cast String Integer`.

`cast` is a function `String -> Integer`, instead of the (more sensible) `String -> Either Integer CastError`.

A really helpful edit would be the V1 and V2 macro expansions; then it's fairly straightforward C with an odd naming scheme.

It's a tiny interpreter. You can create vectors, add them, concatenate them, store them to variables, count their lengths, and so on. An example session:

    x=~5
    5
    0 1 2 3 4
    y=x,x
    10
    0 1 2 3 4 0 1 2 3 4
    x+y
    10
    0 2 4 6 8 0 1 2 3 4

To understand the source, the key are the arrays `C vt[]`, `A(vd[])()`, and `A(vm[])()`, which maps the verb token to the dyads and monads respectively. `V1` functions are monads, `V2` are dyads.

Somewhat facetiously:

    fn identity<T>(t: T) -> T { t }

Has no trait bounds, and is clearly generic. You typically can't do very much with completely free type variables, but Rust has syntactic support for them.

This language is brilliant - at first, it's difficult to believe that such a simple numerical scheme is a programming language. Once you look a bit deeper, you see it's a very clever encoding of a register machine.

Surely philosophy of science helps you build your framework of verifiable, falsifiable statements (after all, you need to have a logical framework for choosing which statements can be falsified or verified)!

So it's something that's not a scientific hypothesis, but is considered knowledge!

(Or, if as in the other comment chain, 1+1=2 is too obvious, you can take any sufficiently non-trivial theorem of your choosing).

But all that says is that 1+1=2 is too obvious. How about some other, less straightforward mathematical theorem, then, like Fermat's Last Theorem.

You can hardly accuse that of being an axiom, or just introducing frameworks of thought.

How do you go about testing the hypothesis that 1 + 1 = 2? Not just showing that a particular physical representation obeys the logical laws of arithmetic, but to test the actual laws themselves.

1+1=2

And no, apples are not the same things as numbers.

You can also give up recursive enumerability. `True Arithmetic`, which takes as axioms all of the true statements in PA is certainly complete and consistent.

This is a strange argument, because all of that rhetoric is status quo - people do argue (or argue via proxy; the words are different, but the substantive claims are the same) that people already receive enough. If that's the problem with universal basic income, then the only change is that such vulnerable people end up with more money, which must be a good thing.

If a struct is public, and all its members are public, you can just create a new instance of the struct with braces (in that case, it would be `OpenSocket { data: 12 }` - or whatever value you like), not what is necessarily correct. By having a hidden zero sized struct member, you need to use the library's api to construct them.

λ calculus is left associative - that is, a sequence of applications A B C is interpreted as (A B) C, so we first reduce (λf x. f (f x)) (λy.* 2 y), yielding λx . (λy. * 2 y) ((λy.2 * y) x), and only then apply 5 to it, which finally lets us unravel everything and get 20.

(Not the OP) I don't know of any examples of using JSON to create types, but here [0] is a practical example of creating types dynamically from input, via writing a type-safe printf:

[0]: https://youtu.be/fVBck2Zngjo

Idris, unlike Haskell, is strict, which has the general effect of making Idris' performance a bit more predictable, and a bit more like programming in other languages.

However, GHC is a phenomenal compiler, and can outperform Idris for many things; this is natural, as it's seen a lot of interest in terms of producing performant code.

There are still some gotchas in Idris code. The biggest one that I can think of is indexing some type with data that doesn't manage to get erased (the usual type erasure algorithm is pretty aggressive, but it can't remove everything). Some of the most useful types for programming (as in, proving theorems about the code) are wonderfully inefficient (as an example, the inductive definition of natural number is an empty linked list - taking up plenty of space in pointers, and killing your cache whenever it's accessed - Idris knows about Nat, but not about other types). Operations on the data, which might look very efficient, can also end up operating on the indices, which might not be.

Here's the docs explaining the possible hiccup with erasure: http://docs.idris-lang.org/en/latest/reference/erasure.html

Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.