Question about terminology: Is it common to call higher-order function types "exponential types" as the article does? I know what higher-order functions are, but am having trouble grasping why the types would be called "exponential".

▲ xigoi 4 days ago | parent | next [-]

ackfoobar has already given a good reason why function types are called exponential, but there is an even deeper reason: function types interact algebraically the same way as exponents.

The type A → (B → C) is isomorphic to (A × B) → C (via currying). This is analogous to the rule (cᵇ)ᵃ = cᵇ˙ᵃ.

The type (A + B) → C is isomorphic to (A → C) × (B → C) (a function with a case expression can be replaced with a pair of functions). This is analogous to the rule cᵃ⁺ᵇ = cᵃ·cᵇ.

	▲	ackfoobar 3 days ago \| parent [-]
		Since the cardinalities match the algebra, it's no surprise that identities translate, but seeing them still brings a smile to my face. The correspondence can be pushed much further - to differentiation! https://codewords.recurse.com/issues/three/algebra-and-calcu...

▲ ackfoobar 5 days ago | parent | prev | next [-]

A first-order function type is already exponential.

A sum type has as many possible values as the sum of its cases. E.g. `A of bool | B of bool` has 2+2=4 values. Similarly for product types and exponential types. E.g. the type bool -> bool has 2^2=4 values (id, not, const true, const false) if you don't think about side effects.

▲ jolmg 5 days ago | parent [-]

> bool -> bool has 2^2=4 values

Not the best example since 2*2=4 also.

How about this bit of Haskell:

  f :: Bool -> Maybe Bool

That's 3 ^ 2 = 9, right?

  f False = Nothing
  f False = Just True
  f False = Just False
  f True = Nothing
  f True = Just True
  f True = Just False

Those are 6. What would be the other 3? or should it actually be a*b=6?

EDIT: Nevermind, I counted wrong. Here are the 9:

  f x = case x of
    True -> Nothing
    False -> Nothing

  f x = case x of
    True -> Nothing
    False -> Just False

  f x = case x of
    True -> Nothing
    False -> Just True

  f x = case x of
    True -> Just False
    False -> Nothing

  f x = case x of
    True -> Just False
    False -> Just False

  f x = case x of
    True -> Just False
    False -> Just True

  f x = case x of
    True -> Just True
    False -> Nothing

  f x = case x of
    True -> Just True
    False -> Just False

  f x = case x of
    True -> Just True
    False -> Just True

▲

ackfoobar 5 days ago | parent | next [-]

Good point, well there's Ordering type built-in in Haskell (LT | EQ | GT). Ordering -> bool has 2^3=8 values (const true, const false, == LT, == EQ, == GT, is_lte, is_gte, ne)

EDIT: now you see why I used the smallest type possible to make my point. Exponentials get big FAST (duh).

	▲	jolmg 3 days ago \| parent [-]
		> now you see why I used the smallest type possible I think the length's worth it for the sake of a crystal clear enumeration.

▲

jasperry 5 days ago | parent | prev [-]

You didn't list all functions, just input-output pairs. Each function is a map from every possible input to an output:

f1 False = Nothing, f1 True = Nothing

f2 False = Nothing, f2 True = Just True

...

This gives the correct 3^2 = 9 functions.

▲ nukifw 5 days ago | parent | prev | next [-]

Usually we speaking only about sum and product (because article usually refers to ADT, so Algebraic Data type). A function is not really Data, so it is not included. But you can use the same tricks (ie: a -> b has arity b^a) to compute the number of potential inhabitant

▲ voidhorse 4 days ago | parent | prev | next [-]

The answers in the replies are all good but the real reason is because in category theory the construct that models function types is called an "exponential product". The choice of that name stems from the reasons explored in the replies, in particular from the fact that the number of total functions from A to B is aka ways determined by an exponent (cardinality of B raised to the power of cardinality of A)

▲ vram22 4 days ago | parent | prev [-]

I had the same doubt.

Here is my uneducated guess:

In math, after sum and product, comes exponent :)

So they may have used that third term in an analogous manner in the example.