873 karma · joined November 3, 2017
Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Even though the people there weren't necessarily violating the site guidelines per se, the commentary that some people were making (e.g. discussion about IP stemming from the murderer's unsubstantiated accusation of plagiarism, or discussion about Japan's culture) felt insensitive and hurt me as someone who was greatly impacted by KyoAni's work. I didn't understand how to express my feelings about this, but the way you describe it ("generic dross") explains it perfectly.
This is an exposition of Martin-Lof's dependent type theory: http://www.cs.nott.ac.uk/~psztxa/mgs-17/notes-mgs17.pdf Section 5 is about Homotopy Type Theory (HoTT), a newer type theory that is still being developed.
Chapter 1 of the HoTT book introduces Martin-Lof's dependent type theory, then the rest of the book covers HoTT-specific topics: https://homotopytypetheory.org/book/
According to the Curry-Howard correspondence and the BHK interpretation of logic, there is a syntactic correspondence between types and logical formulas and between terms and proofs.
Here, the unit type corresponds with truth because it is trivially inhabited with a single inhabitant. The product type A * B is interpreted as logical conjunction because you need a proof of A and a proof of B to inhabit it.
The unit type (true) is the identity of the product type (and). Unit * A = A * Unit = A from an isomorphism perspective. From the category theory point of view, a Cartesian monoidal category is a monoidal category where the tensor product is the categorical product and the unit object is the terminal object. It's no coincidence that the terminal object is written as 1.
So, an n-ary sequence of propositions connected by ANDs is like an n-ary tuple type, and an empty sequence of propositions connected by ANDs is like the nullary tuple type, or in other words the trivially inhabited unit type.
Scratch 3 runs on a modified version of Blockly.
"Sprite" and "costume" are distinct concepts in both Scratch and Snap!. A costume is a texture, and a sprite is an actor associated with state such as a current costume, as well as program logic.
There is a distinction between intensional Martin Lof type theory and extensional Martin Lof type theory, which differ in their treatments of equality. First, one must distinguish between judgmental equality x = y, which is a statement in the mathematical metalanguage that two terms are equal, and propositional equality, which "internalizes" judgmental equality within the programming language through the equality type Id(A, x, y), the type of proofs that x and y are judgmentally equal. In extensional type theory, judgmental equality also follows from propositional equality, and together with the eta-conversion rule for functions, function extensionality is provable [0]. However, typechecking extensional type theory is undecidable [1].
Alternatively, in Homotopy Type Theory (HoTT), supports function extensionality is provable from the univalence axiom, which states that isomorphic types are equal [2]. Function extensionality is trivially provable in Cubical Agda [3], which gives a computational interpretation of HoTT's notion of equality.
[0] https://cstheory.stackexchange.com/questions/46331/extension...
[1] https://cs.stackexchange.com/a/112559
[2] https://ncatlab.org/nlab/show/function+extensionality#relati...
[3] https://agda.readthedocs.io/en/v2.6.0.1/language/cubical.htm...
I also like OCaml because it is both imperative and functional, so I can use the best of both paradigms.
[1] https://caml.inria.fr/pub/docs/manual-ocaml/libref/Stdlib.ht...
This version introduces a new tactic language, Ltac2.
This is only one part of the definition of an applicative. Applicatives must also preserve the monoidal operation (product). That is, there is a function `pair : f a -> f b -> f (a * b)`. Then, you can map functions of multiple arguments by turning `(a * b) -> c` into `f (a * b) -> f c` via `map` and passing it the result of the applicative `pair` operation.
> monad -> equivalent of unwrappering list items, applying a function to each, and rewrapping it
I'm not sure how precise or accurate this definition is. I'd say that a monad is about collapsing multiple layers of a functor into one layer.
> This is just for lists, but the terms are more powerful than that and have many variations. The nice thing is because it's universal. You don't have to wonder, "have I done this pattern right," because you test the laws for them. It might also help, for some of the laws, to remember identity and associativity as like from multiplication -- ie 1 * 9 = 9, 3 * 2 = 2 * 3
Yup, I agree that this is a benefit of generalizing these operations based on their common structure.
Most programmers probably know "map" as being an operation takes a function and a list and returns a list of the results of the function applied to each element of the input list. However, the "map" operation can be generalized to generic types other than lists, where it has different behavior but shares certain properties. In functional programming, the idea of a functor gives a name to this pattern.
The idea is that if you have some generic type `T a` covariant in `a`, there is a function `map : (a -> b) -> T a -> T b` that can "lift" every function `f : a -> b` into a function `map f : T a -> T b`. The lifting operation respects function composition and identity.
However, what if the function has multiple arguments, e.g. `f : a -> (b -> c)`? Then, `map f : T a -> T (b -> c)` An applicative functor lets you convert that `T (b -> c)` into a `T b -> T c`. So, with applicative functors, you can individually map each parameter of a multi-parameter function.
A monad is a functor that can be "flattened." It has an operation `join : T (T a) -> T a`, as well as an operation `return : a -> T a`. A monad can be seen as generalizing the idea of flattening a list, or generalizing async/await.
- A -> B (Function type) and A => B (Logical implication)
- A * B (Product/Tuple type) and A /\ B (Logical conjunction)
- A + B (Sum/Tagged union type) and A \/ B (Logical disjunction)
Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B.
So writing a definition that has a certain type is the same thing as proving a theorem.
Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have:
- The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x.
This is the same thing as universal quantification, "for all x of type A, B(x) holds."
- The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x.
This is the same thing as existential quantification, "there exists an x of type A where B(x) holds."
So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory."
[0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
[1] https://en.wikipedia.org/wiki/Dependent_type
[2] https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...
Types let you to have a "dialogue" with the compiler. Programming in Agda is very much intended to be an interactive experience, via its Emacs mode.
Typed holes in GHC: https://wiki.haskell.org/GHC/Typed_holes
Agda Emacs mode: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm...
In the article, you compare the usage of types to guide you with test-driven development. There is actually a book called Type-Driven Development about using dependent types in the Idris language, although I have not read it. It is written by Edwin Brady, the creator of Idris. https://www.manning.com/books/type-driven-development-with-i...
As @willtim explains, monads were applied to PL theory to model effects. The IO monad models the effect of state, i.e. imperative programs. The type `IO a` is essentially a "wrapper" or "alias" for the type `RealWorld -> (RealWorld, a)`. You should think of the entire world as being the input to a Haskell program.
Haskell does have impure backdoors into IO such as unsafePerformIO, but the IO monad itself is perfectly pure.
P.S. For more information, check out the work of Eugenio Moggi [0], who started using monads to give semantics to programming languages, and Philip Wadler [1], who applied the idea on a programmer-facing level.
[0] https://person.dibris.unige.it/moggi-eugenio/ftp/ic91.pdf
[1] https://groups.csail.mit.edu/pag/OLD/reading-group/wadler-mo...
I'd say that OCaml blends imperative and functional programming cohesively and fairly equally, though.
You should probably link to the videos on your project's website as part of the documentation. You could also make your Show HN a text post and link to the website and the tutorial videos in the body. However, I'd say that merely posting the videos on the website for people to find is more natural.
These are the rules for Show HN: https://news.ycombinator.com/showhn.html
The Sakuga Blog is a publication of Sakugabooru, a booru (image board, https://en.wikipedia.org/wiki/Imageboard#Danbooru-style_boar...) that collects the works of animators.