6 ms·

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a functi

Nice article. I especially liked: > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. Also, I never thought of "higher-order functions" as breaking into a countable hierarchy of nth-order functions, which is an interesting thought. In Haskell the hierarchy would start off as zerothOrderFunction :: a firstOrderFunction :: a -> b SecondOrderFunction :: a -> (b -> c) SecondOrderFunction' :: (a -> b) -> c In general, an nth-order function is a function which either 1. Takes an (n-1)th order function as an input and returns a simple type. 2. Takes a simple type as an input and returns an (n-1)th order function as an output. The upshot is that typed programming languages not only catch bugs, but prevent you from legally expressing many non-sensical expressions (analogous to the set theory paradoxes). For example, consider the expression (\x -> x x) (\x -> x x) If you expand this expression, it reduces to itself: (\x -> x x) (\x -> x x) == (\x -> x x) (\x -> x x) In a purely untyped language, this expression would be legal. But what would be its meaning? Arguably, it is non-sense, and should be excluded from the set of legally expressible expressions. The way to do this is through a type system. And indeed, if you typed this statement into a Haskell REPL you would get a type error; this statement can actually be proven to be untypable (IIRC). On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-)

kmill 9y ago
> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is program3() == runFunction(runFunction) == runFunction(1) == 1(1) == Error: func (with value 1) is not a function
- georgewsinger 9y ago
  I see. The error makes sense now.
- oldandtired 9y ago
  Depending on your system, 1(1) is quite sensible, That is applying 1 to a list of parameters just returns the 1st parameter. This is a matter of the semantics that one uses when application is run against any value. 1(1) -> 1 Just because the common idea of application is that it only applies to functions does not mean that application applied to other types is nonsensical and should end up with a runtime error. If your language allows application to be defined for different types, then the type system should be capable of determining the type that returns from application. A practical example of a language in which application is valid for integers is Unicon/Icon. Both functions and integers have specific semantics with regards to application. And failure is an option.
gizmo686 9y ago
>On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-) Any type system will reject some correct program. As a trivial example, consider: if( f() ): 1 + "a" else 1 This is a perfectly fine expression iff the result of f() is always false.
- georgewsinger 9y ago
  Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").
  - gizmo686 9y ago
    Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case. Or consider a program like: x = 1 print_int(x) x="a" print_string(x) I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify. Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it). You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior. A completely different type of example, is C code such as: *0x01 = 0 which means "set the memory at address 1 to 0", but is poorly typed.
ky3 9y ago
foo :: a -> (b -> c) Not saying it's wrong, but "foo is a second-order function" is a distinctly minority opinion. To a useful first approximation, Haskell works as a cartesian-closed category, which basically means we have tuples and that tuples harmonize with functions so that foo behaves just like uncurry foo :: (a,b) -> c which is a first-order function. So the majority opinion calls foo a first-order arity-2 function. Here's a bar function that's truly second-order: bar :: (a -> b) -> c In general, the order of a function is the count of parens nesting the leftmost innermost arrow. It is invariant to currying/uncurrying as well as permutation of arguments. The same counting principle applies to other invariants such as ranks and kinds. "How high can the order of a function go?" is the question explored in this blog post [0]. Note how the author's definition of order -- essentially the same given here -- got left and right mixed up. [0] http://math.andrej.com/2006/03/21/interesting-higher-order-functionals/ http://math.andrej.com/2006/03/21/interesting-higher-order-f...
- jonsterling 9y ago
  I think it is not just a minority opinion, but just plain wrong.
ky3 9y ago
> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-) Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike in an untyped universe: http://us5.campaign-archive1.com/?u=4937a9a2eb9eee0a26e1e0a23&id=5185ab6f09 http://us5.campaign-archive1.com/?u=4937a9a2eb9eee0a26e1e0a2... In other words, types can sometimes make you lose reuse. That's amply compensated by types removing massive amounts of junk in the untyped world. If you don't believe me, try hacking in an untyped calculus sometime.
- naasking 9y ago
  > Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike an untyped universe: That's an example in one type system, not a feature of all type systems. There's a good argument that typing is more expressive than dynamically typed languages: you can always add a dynamic type to your style system and recover all dynamically typed language features, but you can't go the other way around and recover all the features of a statically typed language. For instance, the performance benefits.
didibus 9y ago
> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. This happens quite often. Take datastructures. It is often very useful to structure different types of data together in a common structure. Now in most cases, you don't know in advance which type will go where in the datastructure, as the data might only be known or derived at runtime. In fact I'd say dynamic behavior is the major expressiveness loss. Granted, I'm not sure how runtime vs static type system relate to type theory. Anyone can educate?
- evincarofautumn 9y ago
  It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic type errors. That would let you do some interesting things like creating a type from runtime data, such as a database schema. It’s just that historically people have found it markedly more useful to have that information available statically, because it lets you prove things about your code that hold “for all” cases (universals), not just “for some” that are executed (existentials). And static information can be used for optimisations because of those guarantees—if you have proof, you don’t need a fallback.
  - catnaroek 9y ago
    You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?
    - evincarofautumn 9y ago
      What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list<T>” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)
lower 9y ago
Your definition of order is not the standard one! Usually one would have: zerothOrderFunction :: a firstOrderFunction :: a -> b firstOrderFunction' :: a -> (b -> c) SecondOrderFunction :: (a -> b) -> c After all, the functions firstOrderFunction and firstOrderFunction' are the same up to currying. The standard definition of order is given here (at the end of the section): https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#T...

kmill 9y ago

> > program3 fails because runFunction can only run first-order functions and runFunction is a second-order function – a function that takes a first-order function as a parameter. > Here I had no idea that JavaScript implicitly typed `runFunction` that way. That's cool. In case it's not clear, it's just that it eventually ends up with a run time error (the talk about runFunction being a second-order function is just an explanation for why you should expect it to end up with a run time error). The evaluation is program3() == runFunction(runFunction) == runFunction(1) == 1(1) == Error: func (with value 1) is not a function

georgewsinger 9y ago
I see. The error makes sense now.
oldandtired 9y ago
Depending on your system, 1(1) is quite sensible, That is applying 1 to a list of parameters just returns the 1st parameter. This is a matter of the semantics that one uses when application is run against any value. 1(1) -> 1 Just because the common idea of application is that it only applies to functions does not mean that application applied to other types is nonsensical and should end up with a runtime error. If your language allows application to be defined for different types, then the type system should be capable of determining the type that returns from application. A practical example of a language in which application is valid for integers is Unicon/Icon. Both functions and integers have specific semantics with regards to application. And failure is an option.

gizmo686 9y ago

georgewsinger 9y ago
Interesting. It could still be argued this program isn't meaningful (or perhaps "not useful").
- gizmo686 9y ago
  Well, it is a trivial example. In reality, such things would be hidden in the complexity of the code. One could argue that if the correctness of the code cannot be accepted by the type system then it would also be confusing for a human to look at, and should therefor be refactored; which is why (in practice) this is a non issue. For a less trivial example, consider the expression "f(x) + g(x)" where both f and g can return either a number or a string. It is conceivable that for any given x, they would always return the same type, but a type system cannot detect every such case. Or consider a program like: x = 1 print_int(x) x="a" print_string(x) I have seen code just like this in dynamically typed languages. You can also run into a simmilar situation that is not obviously correct if, for example, x is a global variable while the program is running a state machine. You can then view each state a transitioning the type of x. Determining if such a program is correct would involve knowing each state transition, what type of x is expected when control enters a state, and what type x is when control leaves a state (and a given state might have multiple output (or even input) types. I have seen one program that actually worked like this; and it was not fun to modify. Of course, a type system is no guarentee that you do not have this sort of problem. For example, you could say, in the first example, that x is a union type of Int and String (and print_int and print_string are defined to operate on such a union). In this case, the program is well typed, but has partial functions, so the type system cannot guarantee that there will not be a runtime error when you call them (it won't, however, be a type error, since the type system missed it). You could also have x be an untagged union. In this case, I don't see a way of doing any better than undefined behavior. A completely different type of example, is C code such as: *0x01 = 0 which means "set the memory at address 1 to 0", but is poorly typed.

ky3 9y ago

foo :: a -> (b -> c) Not saying it's wrong, but "foo is a second-order function" is a distinctly minority opinion. To a useful first approximation, Haskell works as a cartesian-closed category, which basically means we have tuples and that tuples harmonize with functions so that foo behaves just like uncurry foo :: (a,b) -> c which is a first-order function. So the majority opinion calls foo a first-order arity-2 function. Here's a bar function that's truly second-order: bar :: (a -> b) -> c In general, the order of a function is the count of parens nesting the leftmost innermost arrow. It is invariant to currying/uncurrying as well as permutation of arguments. The same counting principle applies to other invariants such as ranks and kinds. "How high can the order of a function go?" is the question explored in this blog post [0]. Note how the author's definition of order -- essentially the same given here -- got left and right mixed up. [0] http://math.andrej.com/2006/03/21/interesting-higher-order-functionals/ http://math.andrej.com/2006/03/21/interesting-higher-order-f...

jonsterling 9y ago
I think it is not just a minority opinion, but just plain wrong.

ky3 9y ago

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. It would therefore be interesting if somebody found an expression which was both (i) meaningful and (ii) only expressible in an untyped language. You would then have an argument for untyped languages :-) Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike in an untyped universe: http://us5.campaign-archive1.com/?u=4937a9a2eb9eee0a26e1e0a23&id=5185ab6f09 http://us5.campaign-archive1.com/?u=4937a9a2eb9eee0a26e1e0a2... In other words, types can sometimes make you lose reuse. That's amply compensated by types removing massive amounts of junk in the untyped world. If you don't believe me, try hacking in an untyped calculus sometime.

naasking 9y ago
> Here's an example: The W combinator `\f x -> f x x` can be expressed in Haskell but it doesn't work everywhere it should, unlike an untyped universe: That's an example in one type system, not a feature of all type systems. There's a good argument that typing is more expressive than dynamically typed languages: you can always add a dynamic type to your style system and recover all dynamically typed language features, but you can't go the other way around and recover all the features of a statically typed language. For instance, the performance benefits.

didibus 9y ago

> On the other hand, this means that typed systems are in some sense strictly less expressive than their untyped counterparts. This happens quite often. Take datastructures. It is often very useful to structure different types of data together in a common structure. Now in most cases, you don't know in advance which type will go where in the datastructure, as the data might only be known or derived at runtime. In fact I'd say dynamic behavior is the major expressiveness loss. Granted, I'm not sure how runtime vs static type system relate to type theory. Anyone can educate?

evincarofautumn 9y ago
It’s partly just coincidence that dynamically typed languages tend to have less expressive type systems. You could run any typechecker at runtime if you wanted. There’s no reason you couldn’t have a Python-like language where the “list” type dynamically keeps track of the types of its elements, function types keep track of the types of their inputs and outputs, and so on, to give you more precise & useful dynamic type errors. That would let you do some interesting things like creating a type from runtime data, such as a database schema. It’s just that historically people have found it markedly more useful to have that information available statically, because it lets you prove things about your code that hold “for all” cases (universals), not just “for some” that are executed (existentials). And static information can be used for optimisations because of those guarantees—if you have proof, you don’t need a fallback.
- catnaroek 9y ago
  You create a reference cell containing an empty list. Because the cell is mutable, it can't have a polymorphic type - it must have a monomorphic one. How do you determine at runtime the type of this cell, before the first time you mutate it?
  - evincarofautumn 9y ago
    What I’m suggesting is that you could literally just run HM or another typechecker at runtime. You’d give an empty list the type “list<T>” for a fresh type variable T; appending an integer would introduce the constraint T = int; appending a string would introduce T = string and raise a runtime error. (Or not—it’s up to the typechecker if it wants to degrade to “int|string” or something.)

lower 9y ago

Your definition of order is not the standard one! Usually one would have: zerothOrderFunction :: a firstOrderFunction :: a -> b firstOrderFunction' :: a -> (b -> c) SecondOrderFunction :: (a -> b) -> c After all, the functions firstOrderFunction and firstOrderFunction' are the same up to currying. The standard definition of order is given here (at the end of the section): https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#Typing_rules https://en.wikipedia.org/wiki/Simply_typed_lambda_calculus#T...