4 ms·

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, bu

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".

nukifw 1y ago
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
ackfoobar 1y ago
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 1y ago
  > 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 1y ago
    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 1y ago
      > 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 1y ago
    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.
vram22 1y ago
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.
xigoi 1y ago
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 1y ago
  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-calculus-of-algebraic-data-types https://codewords.recurse.com/issues/three/algebra-and-calcu...
voidhorse 1y ago
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)

nukifw 1y ago

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

ackfoobar 1y ago

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 1y ago
> 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 1y ago
  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 1y ago
    > 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 1y ago
  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.

vram22 1y ago

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.

xigoi 1y ago

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 1y ago
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-calculus-of-algebraic-data-types https://codewords.recurse.com/issues/three/algebra-and-calcu...

voidhorse 1y ago

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)