873 karma · joined November 3, 2017
I like OCaml because it strikes a balance between imperative and functional programming. Maybe learning OCaml would be easier than learning Haskell?
(Plus, OCaml has neat features like polymorphic variants and a powerful module system!)
Back when I didn't understand what a monad was, I would read a bunch of tutorials and get confused by the analogies and examples. For example, I would get confused by comparisons to "boxes," or I would think that Maybe was the definition of a monad, or that IO was the definition of a monad.
The information in the tutorial that you link seems to be all correct. However, it's too "jumpy" for my tastes. The tutorial talks about "contexts," but doesn't really explain what a "context" is, except for making a comparison to "boxes." I get that a functor is an abstract idea, so explaining it in an understandable way is difficult. However, I wish that the article would discuss type constructors, because the idea of mapping types to types is an important part of the definition of functor. Without this explanation, I imagine that the comparison to "boxes" would have given the past me the wrong impression of what a functor is.
In my tutorial, I sought to teach the actual definition of a functor, applicative, and monad. I explain that a functor maps types to types and functions to functions in a way that preserves composition and identity, that an applicative preserves the product, and that a monad is characterized by a "join" operation that "flattens" the data and a "return" operation that "wraps up" the data. I actually would have preferred to explain the actual category theory, but I felt that it would be too intimidating, and so I attempted to convey the ideas in a non-category-theory way. With my current understanding of functor, applicative, and monad, I believe that if one doesn't learn their actual definitions, one doesn't truly understand them. I guess that I wanted my tutorial to be more rigorous.
However, I am not an expert on teaching, so maybe I'm taking the wrong approach.
See my Reddit comment: https://www.reddit.com/r/programming/comments/cy35zz/functor...
It seems that the computational essay is a step higher than ordinary literate programming, as the code is executable in the format being used to present the document.
Reading this submission reminded me of this interactive article on coeffects, which fits the description of a computational essay: http://tomasp.net/coeffects/
P.S. Are you the same person who submitted this on Reddit?
Standard ML (SML) is a typed functional programming language from the ML family (the same family that OCaml is from). SML doesn't seem to receive the same spotlight that OCaml and Haskell do, so it's cool to see an SML project.
Reddit discussion: https://www.reddit.com/r/programming/comments/d1es7v/try_sta...
Constructive math is a philosophy of math where you must construct a value to proof its existence. The Intermediate Value Theorem states that if f(a) < 0 and f(b) > 0, then there exists a number c in the interval (a, b) where f(c) = 0. For the IVT to be constructive, you must be able to find c. (Technically, the theorem is Bolzano's theorem, not the IVT.)
The question asks why the Intermediate Value Theorem isn't constructive. The question provides a "binary search" for c.
The answer states that the proof doesn't work because checking whether a real number is 0 is undecidable. A real number is represented by an infinite sequence, and you can't tell if the sequence converges to 0.
Reddit discussion: https://www.reddit.com/r/programming/comments/cy35zz/functor...
My HN submission (which didn't receive any traction): https://news.ycombinator.com/item?id=20850144
As for BuckleScript, I wish that it had better integration with the main OCaml ecosystem. BuckleScript is supposed to work well with NPM, but I am more interested in OPAM. I personally use js_of_ocaml, a compiler to JavaScript that works well with the OCaml tooling.
If Reason and BuckleScript can bring more people to OCaml, then I'm glad. However, I perceive that the people coming to OCaml with BuckleScript seem to be making libraries based around the NPM ecosystem. I feel worried that a separate OCaml ecosystem will come into existence. However, I have not observed any other OCamller voice these thoughts, so I'm probably alone or misinformed here. I'm not too knowledgeable about the JavaScript trends.
Your comment refers to me as an "OCaml person." Please know that these opinions are my own and do not in any way represent the collective OCaml community's opinion on Reason and BuckleScript.
The most striking difference is that OCaml has the ML module system, where you can have functions from modules to modules. F# doesn't.
Recent versions of OCaml now have features like first-class modules and binding operators. AFAIK F# has not added them.
On the other hand, F# has features that OCaml doesn't, such as computation expressions, strongly typed units of measure, and active patterns.
I learn type theory from reading on the Internet. My father is a programmer, but he mainly uses C++, so he wouldn't know type theory.
To be honest, I probably wouldn't have learned about type theory if it weren't for the Advanced Topics subculture. My first exposure to programming was with Scratch, and on the Scratch "Advanced Topics" forum (ATs), there is a subculture of people (ATers) who are more knowledgeable about programming than the average user and enjoy pushing Scratch to its limits. (I guess you could say that the ATers are hackers.) One of my friends from the ATs is interested in programming language stuff, and many people there are Lisp hackers. So, the poeple in the ATs are probably responsible for stimulating my curiosity and directing me towards functional programming and PL theory. However, I wouldn't say that I learned type theory from the ATs.
Oh yeah, I also learn type theory from people on the Fediverse (the federated social network that Mastodon uses), as there are people there who are knowleadgable about type theory.
In type theory, there are things called "terms" and "types." A term is something like `fun x -> x`, or `(1, 2)`, or `1 + 1`. In short, a term is basically an expression. Each term has a type. For example, `fun x -> x` might have the type `a -> a` and `(1, 2)` might have type `Nat * Nat`. If a term has a type, it "inhabits" the type. "x has type T" is written `x : T`.
According to an idea called the Curry-Howard correspondence, types can encode logical statements such that terms that inhabit the type are its proofs. Therefore, by inhabiting a type, you are really proving a theorem.
With dependent types, the term and type languages are the same language, so you can mix them together. In short, types are terms.
Here are some types in Martin-Lof type theory:
---------
() : Unit
x : A y : B
--------------
(x, y) : A * B
x : Empty
----------------
elim-empty x : a
x : A
--------------
Inl x : A + B
x : B
--------------
Inr x : A + B
f : A -> B x : A
-------------------
f(x) : B
With dependent types, the product and exponential types are generalized into the dependent sum (sigma) and the dependent product (pi) types respectively.
With the dependent sum type, or sigma type `Σ (x : A) B(x)`, the second component in the type is actually a function of A (meaning that B : A -> Type). The dependent sum type generalizes the product type so that the type of the second element of the pair is actually dependent on the first element. In the Curry-Howard correspondence, the sigma type corresponds with existential quantification, "there exists" or "for some." To prove Σ (x : A) B(x), you must inhabit A (show that A exists) and B(x) (where B is a logical statement about x, the inhabitant of A).
With the dependent product type, or pi type `Π (x : A) B(x)`, B is also a function of A that returns a type. The dependent product type generalizes the exponential type so that the codomain of the function, B(x), is dependent on the function's input, x. The dependent product type corresponds with universal quantification, "for all." To prove Π (x : A) B(x), you must prove B(x) for every possible x, where B(x) is a logical statement about x.
Why the dependent product type generalizes the exponential type and the dependent sum type generalizes the product type seems confusing at first glance, but it really isn't:
Σ for x = 1 to n, B(x) = B(1) + B(2) + ... B(n), and if B(x) is some constant C, Σ for x = 1 to n, C = n * C. The same rule applies to types, as multiplication (product) is just repeated addition (dependent sum of a constant).
Π is like Σ, but for repeated multiplication instead of repeated addition. After all, exponentiation is just repeated multiplication.
Another type that you should be aware of is the equality type, `x = y`. In vanilla Martin-Lof type theory, `x = y` is inhabited by `Refl` if `x` and `y` have the same normal form (reduce to the same simplest form). However, there is ongoing research in a field called Homotopy Type Theory, which redefines the equality type in various ways.
Finally, types themselves form a hierarchy. With dependent types, the types themselves are first-class values, and they have their own types. However, `Type : Type` leads to Girard's paradox (similar to Russell's paradox). The solution is for each type to be in a "universe" so that `Type l : Type (l + 1)`, where `l` is the universe level.
Read about Martin-Lof type theory: https://en.wikipedia.org/wiki/Intuitionistic_type_theory
Agda and Coq are pure functional languages, and their type systems are a consistent logical system. They are more mathematically oriented and may not be what you want.
Agda Emacs: https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.htm...
Coq Tactics: https://coq.inria.fr/refman/proof-engine/tactics.html
f :: (a -> b -> c) -> b -> a -> c
f (+) 1 2
"cookie"
The in-development GP language can alternate between blocks and text: https://en.scratch-wiki.info/wiki/GP_(programming_language)
The 4.08.0 release also adds the Fun, Option, and Result modules to the standard library.
> Objection 1. Data structure and functions should not be bound together
In languages like OCaml and C, one defines types separately from functions. Sometimes, however, I find that a function is best associated with a particular type. In OCaml, that's one purpose of modules. (The convention is to call the main type "t.") However, this organization shouldn't be forced on you.
> Objection 2. Everything has to be an object.
This objection only applies to languages like Java that force OO on you. In OCaml or C++, I don't have to use OO, but I still can if I want to.
> Objection 3. In an OOPL data type definitions are spread out all over the place.
Armstrong complains about having to decide what to inherit from when making a Time object. IMO this is a strawman; in Java, classes inherit from Object by default and I don't see any inconvenience. I do agree that it can be annoying that Time has to be object-oriented, and this is where the benefit of OO being voluntary comes in.
> Objection 4. Objects have private state.
I either disagree with or don't understand this objection. Dr. Armstrong lists three ways to deal with state.
His third option is to use pure functional programming. I see both the beauty and practical value in making functions be functions in the math sense, that is to say, mappings from elements of the domain to elements of the codomain. Then, you get equational reasoning. I am sympathetic to this idea. Nevertheless, languages like Haskell aren't for everybody.
His second option is to control access to mutable variables with scope. You can implement a pure function in an imperative way, and that can be a form of encapsulation. This is a good approach, too.
Dr. Armstrong's first option, which he says is the worst, is the idea that objects maintain hidden state which people control via methods. To me, this isn't about state, but rather encapsulation and abstraction. The idea is that when one, say, inserts into a hash table, the person doesn't think about the implementation ("hash the key and walk down the corresponding bucket"), the person thinks of the abstract problem domain ("map this key to this value"). The hash table interface hides its internal state behind the methods. Even in a programming language like C, one writes functions that operate on, and mutate, structs to abstract things away.
Although the second option is good, I see it as orthogonal to the first option, not a superior alternative. If you are going to confine state to within a function, ultimately, don't you have to do mutations on the local variables, and therefore call some kind of method or impure function on them? However, perhaps I am misunderstanding this fourth point.
A lot of arguments, including this submission, pit OOP against FP and argue that FP is superior to OOP. Even though I use FP, I also think that OOP can be useful. They are not opposites and don't have to conflict.
OCaml is infamous for its object layer, yet I ended up using it for a project. I wanted to describe UI "widgets" such that I could compose arbitrary different types of widgets. Before deciding on objects, I had considered first-class modules or a record of functions, but ultimately decided that objects were the most readable choice.
In my OCaml program, I mainly viewed OOP as a way to abstract different types into a common idea. Widgets are all different, and they have different behaviors, but they all have a position in space, a length, and a width. One can also reposition them (mutation!). To me, the purpose of OO is to express ideas such as these. I note that when I used OOP here, I cared less about state and more about the abstraction of what a "widget" was, via dynamic dispatch. It is bad when the language forces OO on you, but it has valid uses.