TheAsprngHacker

> You can count the number of type systems that are "logically OK" (the formal terms are sound (doesn't admit wrong programs, unlike e.g. Java), complete (can admit all correct programs (for some definition of "correct"), unlike e.g. Scala)... on one hand. The rest amount to various amounts of hacks

Huh? Rice's Theorem states that any static semantic analysis must either reject valid programs or accept invalid programs. This says nothing about whether a type system is rigorous or hacky.

> common ones include specifying function parameter types to allow type inference to function

It's true that type inference becomes undecidable without annotations for things like dependent types, and there's nothing hacky about that.

I use OCaml, and monads also come up in OCaml code. Monads may not be as essential to understand in OCaml than in Haskell because OCaml doesn't use them to track IO in the type system, but people use them in OCaml to chain options and results. In fact, OCaml 4.08 introduced syntactic sugar that makes functor, applicative, monad usage more convenient. I'd say that monads are something that non-Haskell functional programmers should learn.

Monads also turn up with lists (flatmapping) and promises. Although you don't need to know what a monad is to flatmap a list or use promises, I'd say that being aware that lists have a monad instance or that promises have a monad instance provides insight.

If you're new to functional programming, you don't need to worry about the category theory definition. Especially since this tutorial simply mentions it as a way to say, "this is too complicated for us, so we're going to explain it another way," and makes no attempt to break down the definition as code. In fact, be careful that you're not seeing category theory definition and misunderstanding it to confirm a mistaken intuition.

The category-theoretic definition basically states that a monad is an endofunctor T equipped with two operations, return :: a -> T a and join :: T (T a) -> T a. T being a endofunctor just means that it is "mappable," AKA it has a function fmap :: (a -> b) -> T a -> T b that "lifts" functions into the type.

Monads capture the idea of flattening. If fmap changes the "contents" while preserving the "shape," join collapses nested layers to change the "shape."

Instead of join, the Haskell typeclasses (and this article) uses another function called bind, or >>=. You can derive join from >>=, and you can derive >>= from join and fmap. For lists, a more familiar name for >>= might be flatmap.

The ML family and Haskell are good for writing compilers because sum types and pattern matching lend themselves well to ASTs and symbolic manipulation. OCaml and Haskell have been used for real-world language projects (OCaml is used to implement OCaml, Coq, Haxe, Hack, and was used to implement the original version of Rust, and Haskell is used to implement GHC, Elm, PureScript, Agda, and Idris.). I'm making a programming language in OCaml, and I quite like the experience. I've never used Prolog, though.

Discussion on r/math: https://www.reddit.com/r/math/comments/dzbmbu/a_new_way_to_s...

In my code, the Z doesn't mean integer; it stands for zero. Nat is an inductive type, and Z is the base case. Z has type Nat.

> There's no ADT in category theory. The only place you might find them is in type theory

I wouldn't say that this is true. Category theory has a definition of product of objects, sum/coproduct of objects, terminal object (unit type), and initial object (empty type). There is a correspondence between type and category theory where a certain type theory is the internal language of a certain category: https://ncatlab.org/nlab/show/computational+trinitarianism

Product: https://ncatlab.org/nlab/show/cartesian+product

Coproduct: https://ncatlab.org/nlab/show/coproduct

Terminal object: https://ncatlab.org/nlab/show/terminal+object

Initial object: https://ncatlab.org/nlab/show/initial+object

First, here is a note about the notation that I will use here: Let `1` denote the unit type, the type with one inhabitant. Let `()` denote the inhabitant of the unit type. Let `a + b` or `Either a b` denote the sum of types `a` and `b`. Let `Left` and `Right` be the constructors of the sum type.

Before defining the integers, one must define the natural numbers. Natural numbers are defined as an inductive type, which is a little different from an ordinary sum type:

    data Nat = Z | Suc Nat

Here is another way of defining them. Start by removing the self-reference:

    data NatF a = Z | Suc a

Notice that NatF is the same thing as the Maybe/Option type, AKA 1+a, AKA the sum of the unit type and a.

Given a "fix" type:

    data Fix f = MkFix (f (Fix f))

the definition of the natural numbers would be:

    type Nat = Fix NatF

An "F-algebra" is a way of defining some algebraic structure or data type as a map from a "sum of products" to the type. More precisely, an F-algebra consists of an "object" (type) A and a map F(A) -> A. For the natural numbers, the F is NatF and the map would be a function mkNat : NatF Nat -> Nat, AKA mkNat : (Maybe Nat) -> Nat or mkNat : (1 + Nat) -> Nat.

Related links:

- https://ncatlab.org/nlab/show/inductive+type

- https://ncatlab.org/nlab/show/natural+numbers+object

- https://ncatlab.org/nlab/show/initial+algebra+of+an+endofunc...

- https://en.wikipedia.org/wiki/F-algebra

---

One way of defining the integers is as the product of the natural numbers with themselves, or Nat * Nat, equipped with an equivalence relation ~ where

(a, b) ~ (c, d) := a + d = b + c

(a, b) can be understood as a - b. Of course, a - b = c - d <-> a + d = b + c.

Another way of defining the integers is as:

    data Int = Neg Nat | Zero | Pos Nat

where 0 = Zero, -1 = Neg Z, and +1 = Pos Z.

---

Booleans can be defined as 1 + 1. Left () = True and Right () = False, or vice versa.

Hmm, why isn't this appearing on the Ask HN page?

Huh? A monad isn't a sealed class, it's a generic type equipped with the functions bind and return...

The fact that the name "Yuri" is on this list is interesting because "Yuri" is both a masculine Slavic name and a feminine Japanese name. The rapid switch could be due to the growth or decline of one of these names, where the two usages of Yuri are distinct (from different languages), as opposed to one name whose associated gender changed.

As a disclaimer, I do not believe I've ever seen a captcha when logging in to GitLab. But according to https://docs.gitlab.com/ee/integration/recaptcha.html, you use reCAPTCHA?

Are you aware of the privacy concerns surrounding reCAPTCHA? https://en.wikipedia.org/wiki/ReCAPTCHA#Criticism

I'm very confused about what this blog post is trying to argue. Most of what it discusses isn't related to the Curry-Howard correspondence at all?

At the risk of sounding anti-intellectual, perhaps Orwell's "Politics and the English Language" [0] is relevant here?

[0] http://www.orwell.ru/library/essays/politics/english/e_polit

To be honest, I didn't know about the RAML you link until I read your comment. Would this RAML be common knowledge for people who aren't web developers / don't regularly use web APIs?

Agreed, and Scratch is hardly the pinnacle of programming language theory.

I was talking to professor Shriram Krishnamurthi a week ago about a block-based, educational ML dialect I was making, and he told me that he believed that once a language had a type system as sophisticated as mine, its target audience should be using text, not blocks. So, perhaps Scratch-style languages are a dead-end, or infeasible beyond a certain level.

My personal hope for the "next level" of programming languages is those that use typed holes to interactively help the programmer construct the program.

Calling it topology can be misleading, as HoTT only considers types as spaces in the sense of homotopy equivalence.

Homotopy Type Theory is based on Martin-Lof Type Theory (which is your standard dependent type theory), but reinterprets equality to mean homotopy equivalence. In vanilla MLTT, a = b is inhabited iff a and b share the same normal form, and its proof is refl (reflexivity). In HoTT, a = b may be inhabited by proofs other than refl. Namely, the univalence axiom states that types are equal when they are isomorphic, and function extensionality states that functions are equal when they map the same inputs to the same outputs. You also get higher inductive types, which allow you to define constructors of equalities on inductive types. So, HoTT allows you to prove things that you can't prove under ordinary MLTT.

As someone who's never used Lean, but has played around with Coq and Agda, how do they compare?

The ML programming language is known for its advanced module system. First, you have structured, which are your traditional idea of a module. Structures define types and data. Signatures describe the interface of a module and are like the module's "type." By making types abstract or not mentioning members, signatures achieve encapsulation of modules. Finally, you have functors, which are functions from modules to modules. The parameter is constrained by a signature, and the client can pass any module that conforms to the signature to get an output module that uses the passed module in its implementation.

The module system is used when a type must support certain operations. For example, the Set module (https://caml.inria.fr/pub/docs/manual-ocaml/libref/Set.html) defines a signature called OrderedType for types equipped with a comparison function, and any module that implements OrderedType can be used to make a set.

Notably, ML modules differ from Haskell typeclasses because more than one module can exist for the same combination of types. However, you must pass ML modules explicitly, whereas typeclass instances are passed implicitly. So, ML modules have more power than typeclasses, but at the cost of convenience.

Here is an example where modules are used to make a set:

    module LtInt = struct
      type t = int
      (* Use built-in polymorphic comparison *)
      let compare = compare
    end

    module GtInt = struct
      type t = int
      let compare lhs rhs = compare rhs lhs
    end

    module LtIntSet = Set.Make(LtInt)

    module GtIntSet = Set.Make(GtInt)

However, modules can quickly get inconvenient:

    module type Monoid = sig
      type t
      val op : t -> t -> t
      val e : t
    end

    module Addition = struct
      type t = int
      let op = (+)
      let e = 0
    end

    module Multiplication = struct
      type t = int
      let op = ( * )
      let e = 1
    end

    module FoldLeft (M : Monoid) = struct
      let fold_left = List.fold_left M.op M.e
    end

Here, it's probably less verbose to just pass the operation and starting value directly to List.fold_left than to use modules! Debatably, this is as equally inconvenient as Haskell's newtype solution to multiple instances, but if there is only one instance, typeclasses are much cleaner to use.

Modular implicits are a long-awaited feature that will allow ML modules to be passed implicitly.

https://www.cl.cam.ac.uk/~jdy22/papers/modular-implicits.pdf

The OCaml type 'a * 'b is the equivalent of the Haskell type (a, b). This type is known as the Cartesian product type, and it's written with a multiplication symbol in type theory (hence the asterisk in OCaml syntax).

The product type is the type of pairs. It's definition is

    x : A
    y : B
    --------------
    (x, y) : A * B

meaning that if x has type A and y has type B, then (x, y) has type A * B.

- Product type on Wikipedia: https://en.wikipedia.org/wiki/Product_type - Product type on the nLab (which is a math-heavy resource): https://ncatlab.org/nlab/show/product+type

Thank you for pointing out contravariant functors; I have fixed that sentence in my post and credited you.

I can try to explain this to you from a math perspective, if you want, but I need to know your math background. Are you familiar with the lambda calculus and its relationship to category theory?

The other person also mentioned this. It's called invariance. There's also a fourth variance: https://www.benjamin.pizza/posts/2019-01-11-the-fourth-type-...

Isomorphism is not about currying. When I mentioned isomorphism, I was referring to the interchangeability in general, and the currying relationship is just an example of an isomorphism. In category theory notation:

Hom(A * B, C) ~ Hom(A, C ^ B)

This is one of the laws of a Cartesian closed category. The simply typed lambda calculus with products is the internal language of a Cartesian-closed category.

Thank you for the praise. For me, the inline code has about the same font size as the surrounding text, maybe smaller, and the block code has a bigger font. Is it possible for you to send me a screenshot?

I'm a little confused by your last paragraph. My last code example doesn't use readFile and putStrLn, and it isn't written in Haskell?

In your opinion, is this article less helpful than the functor/monad tutorials that predominantly use Haskell?

Thanks. I know what contravariant functors are, but I haven't used them, so I didn't realize that was what the parent commenter was asking about.

You're right, my claim that every type 'a t has a corresponding (covariant) functor is incorrect, and I should either take that out or mention contravariant functors.

If there is a function `map : ('a -> 'b) -> 'a t -> 'b t`, and there exists a function `x : 'w -> bool`, then `map x : `'w t -> bool t`. Is this what you were asking?

Huh? I cover this definition in the tutorial, when I discuss OCaml's (and+) operator! Did I gloss over things too quickly?

Shrugs Well, Python is dynamically typed and C doesn't really have good polymorphism or first-class function support. Both polymorphism and first-class functions (with closures) are important for understanding functors, applicatives, and monads.

I admit that I'm more fluent in OCaml than I am in Python or C, so please correct me if I'm mistaken.