what are typed programming languages disfavored when doing nks?
gottleb frege in 1893 wrote "basic laws of arithmetic", trying to find the fundamental laws of mathematics. in 1901 bertrand russel found a question that led to a contradiction in frege's scheme (the question was whether a set was a member of itself). russel proposed a patch to frege's system, introducing the notion of a "type" for a set. say a set of numbers is type 1, and a set of sets is type 2. if a is a member of b, then a has to have a smaller type than b. that avoids the contraction inherent in frege's system when you try to answer whether a set is a member of itself (the sets have the same type).
types in programming languages. associate types with variables, just like for sets in russel's scheme. only inputs of certain types are allowed, which makes error checking much easier. the C programming languages is full of type definitions.
in C, strlen(x) gives you the length of string x. C was an improvement of the B language, because it introduced types. strlen(7) gives an error in C.
lambda calculus was the first programming language, written by alonzo church in 1936. it's an untyped language, and is computationally universal. but if you add types, it's no longer universal! (you can only compute polynomials). that's why we avoid typed languages in nks, because we want to combine parts of computations in arbitrary ways. Mathematica is basically an untyped language (weakly typed really). e.g. The Length function works for both Length[{1,2,3,4,5,6}] -> 6, and Length[f[1,2,3,f[4,5]]] (accepts things with arbitrary heads).
wiktor made the point that the only really untyped language is assembler.
someone else made the comment that russel's system fell apart when trying to consider the set of all types (i think).
Comments