3 ms·

This strikes me as a quite language-specific treatise, and may indicate a shortcoming or particularity of the syntax or semantics of the described programming l

by triska 5y ago

This strikes me as a quite language-specific treatise, and may indicate a shortcoming or particularity of the syntax or semantics of the described programming language (i.e., Disco) rather than an essential conceptual difference. For comparison, in Prolog, a type is indeed a set of terms! For example, the type "integer" truly denotes the set of integers, and if an argument has the type "integer", then we know that the predicate can only hold if that argument is an element of this type. Quoting from the Prolog ISO standard: 7.1 Types The type of any term is determined by its abstract syntax (6.1.2). Every term has one of the following mutually-exclusive types: V (variables), I (integers), F (floating point values), A (atoms), CT (compound terms). A term with type I, F, or A is an atomic term. and further: 7.1.2 Integer An integer is a member of a set I (see 6.1.2 c) where I is a subset of ℤ characterized by one or three parameters. Prolog also has type errors: "There shall be a Type Error when the type of an argument or one of its components is incorrect, but not a variable." For example, in Scryer Prolog, we get: ?- length(Ls, a). caught: error(type_error(integer,a),length/2) This is because the second argument of length/2 must be an element of the set I of integers. Since the atom 'a' is not an integer, the relation does not hold in this case. Declaratively, a type error is equivalent to silent failure: It means that the relation cannot hold for this type of argument, and so every specialization of the query will also not hold, whereas a generalization or an instantiation with a term of a different type may succeed. This view readily carries over to logic variables. For example, using library(clpz), we get: ?- X #> 3. clpz:(X in 4..sup). And we get a type error if we try to instantiate the thus constrained variable X to a term that is not an element of ℤ: ?- X #> 3, X = a. caught: error(type_error(integer,a),unknown(a)-1) So, indeed, types denote sets of terms that are acceptable as arguments. The example in the article, i.e., ℕ, could be regarded as an element of the set of atoms in Prolog, and therefore have the type atom. In indeed, for example Trealla Prolog answers: ?- atom(ℕ). true.

elliekelly 5y ago
Only tangentially related, every once in a while I look for a book, video, or even course that concisely explains the “language” of mathematical notation. As someone who is largely self-taught when it comes to the more advanced math it’s frustrating that so many resources assume a basic level of notational knowledge/understanding so they just skip right over it and you’re left piecing it together using context clues and LaTex crib sheets.
- kmill 5y ago
  For better or for worse, piecing things together using context clues never seems to really end :-) One useful heuristic is the "unambiguous parse rule." You think about different ways something might be read (even if you have no idea what it's trying to say yet) and try to work out which one would lead to the least ambiguity. This is helpful also when trying to figure out how to write using newly learned notation yourself. A good technique is to just not get frustrated. All math starts impenetrable. Read ahead, try to get a glimpse of an idea of what's going on. Go back, find other sources about the same thing, find sources about similar things. If the original source was worth anything, eventually it'll reveal itself. Sometimes you realize you weren't the target audience and you were supposed to have been exposed to more introductory material and you wish they had cited one, but anyway, you found it. Another thing is that sometimes you just need to ask an expert, someone who's steeped in the culture. math.stackexchange.com is open to notation questions, but the guidance you can get in-person can be much more nuanced. I actually like running into new notation (supposing I'm not on a deadline trying to figure something out...), be it math or a programming language. You're trying to solve the puzzle of the purpose of the notation, what function does it serve, why someone ever thought this was a good idea. I've exposed myself to a lot of bits of obscure programming languages over the years, which makes it easier to guess what things might mean. Maybe one more thing: math notation tends to be invented for specific purposes, and maybe most of it doesn't carry over from subject to subject. Arithmetic, function application, summations, integrals, and set notation are fairly universal though.
tel 5y ago
This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time". The idea of a runtime procedure `?- atom(_)` which determines `true.` or `false.` is fundamentally an extrinsic property, thus "set like". Intrinsically defined objects are defined through (possibly inductive) construction or (possibly coinductive) destruction rules. Typically a notion of set arises from having some larger universe of things and restricting them via predicates. The notion of types arises from having a system of building (co)inductive definitions and then utilizing that system. Sets are thus, in a sense, fundamentally based on a closed world (said universe) and types an open world (each new utilization of the rules system introduces a novel type).
kmill 5y ago
The word "type" is very overloaded. In the language of type theory, Prolog (and many other languages, usually dynamic) consider a universal type of all terms, and then a "type" is a set on the universal type. This is a fine way to go (though you can get contradictions in the form of infinite loops in typechecking if "types" are terms themselves). In type theory, at least for the ones many theoreticians seem to be interested in, the has_type/2 predicate (using Prolog terminology) is a function, which is to say has_type(x, y) has a single value for y for any given term x. Things are set up so that the way in which x is represented (i.e., constructed) determines y. This is useful computationally because if you know something's type, you then know how to deconstruct it into components. For example, types drive the expected cases of a match expression. My main point with this comment is to bring up the fact that the article is talking about type theories as academics who study functional programming languages see them, so in context it's not specific to Disco. (I should mention that has_type is only a function given a symbolic representation of a construction for x. Theoretically, things of different types can have the same internal representation, like with Java generics or C structs, but I think you can always arrange things so that has_type is a function by tagging values with their type. Even in more delicate dependent type systems.) (I guess I should mention that my understanding of types after some years of confusion is that in the end they essentially provide an API for values. The program code sort of constitutes a proof that a value has a specific type, and then you can interact with it as such. It's explicitly not part of the API for a type to be able to tell whether something has that type -- in many type theories, values can have multiple types! Sets on the other hand are a type where part of their API is that values can determine whether or not a value is an element. It's certainly possible to fuse the concepts so that types are required to be sets, but I think this is avoided because there's not always an algorithm for the set interface.)

by triska 5y ago

elliekelly 5y ago

Only tangentially related, every once in a while I look for a book, video, or even course that concisely explains the “language” of mathematical notation. As someone who is largely self-taught when it comes to the more advanced math it’s frustrating that so many resources assume a basic level of notational knowledge/understanding so they just skip right over it and you’re left piecing it together using context clues and LaTex crib sheets.

kmill 5y ago
For better or for worse, piecing things together using context clues never seems to really end :-) One useful heuristic is the "unambiguous parse rule." You think about different ways something might be read (even if you have no idea what it's trying to say yet) and try to work out which one would lead to the least ambiguity. This is helpful also when trying to figure out how to write using newly learned notation yourself. A good technique is to just not get frustrated. All math starts impenetrable. Read ahead, try to get a glimpse of an idea of what's going on. Go back, find other sources about the same thing, find sources about similar things. If the original source was worth anything, eventually it'll reveal itself. Sometimes you realize you weren't the target audience and you were supposed to have been exposed to more introductory material and you wish they had cited one, but anyway, you found it. Another thing is that sometimes you just need to ask an expert, someone who's steeped in the culture. math.stackexchange.com is open to notation questions, but the guidance you can get in-person can be much more nuanced. I actually like running into new notation (supposing I'm not on a deadline trying to figure something out...), be it math or a programming language. You're trying to solve the puzzle of the purpose of the notation, what function does it serve, why someone ever thought this was a good idea. I've exposed myself to a lot of bits of obscure programming languages over the years, which makes it easier to guess what things might mean. Maybe one more thing: math notation tends to be invented for specific purposes, and maybe most of it doesn't carry over from subject to subject. Arithmetic, function application, summations, integrals, and set notation are fairly universal though.

tel 5y ago

This is an old yarn distinguishing sets and types, extrinsic and intrinsic, "run time" and "compile time". The idea of a runtime procedure `?- atom(_)` which determines `true.` or `false.` is fundamentally an extrinsic property, thus "set like". Intrinsically defined objects are defined through (possibly inductive) construction or (possibly coinductive) destruction rules. Typically a notion of set arises from having some larger universe of things and restricting them via predicates. The notion of types arises from having a system of building (co)inductive definitions and then utilizing that system. Sets are thus, in a sense, fundamentally based on a closed world (said universe) and types an open world (each new utilization of the rules system introduces a novel type).

kmill 5y ago

The word "type" is very overloaded. In the language of type theory, Prolog (and many other languages, usually dynamic) consider a universal type of all terms, and then a "type" is a set on the universal type. This is a fine way to go (though you can get contradictions in the form of infinite loops in typechecking if "types" are terms themselves). In type theory, at least for the ones many theoreticians seem to be interested in, the has_type/2 predicate (using Prolog terminology) is a function, which is to say has_type(x, y) has a single value for y for any given term x. Things are set up so that the way in which x is represented (i.e., constructed) determines y. This is useful computationally because if you know something's type, you then know how to deconstruct it into components. For example, types drive the expected cases of a match expression. My main point with this comment is to bring up the fact that the article is talking about type theories as academics who study functional programming languages see them, so in context it's not specific to Disco. (I should mention that has_type is only a function given a symbolic representation of a construction for x. Theoretically, things of different types can have the same internal representation, like with Java generics or C structs, but I think you can always arrange things so that has_type is a function by tagging values with their type. Even in more delicate dependent type systems.) (I guess I should mention that my understanding of types after some years of confusion is that in the end they essentially provide an API for values. The program code sort of constitutes a proof that a value has a specific type, and then you can interact with it as such. It's explicitly not part of the API for a type to be able to tell whether something has that type -- in many type theories, values can have multiple types! Sets on the other hand are a type where part of their API is that values can determine whether or not a value is an element. It's certainly possible to fuse the concepts so that types are required to be sets, but I think this is avoided because there's not always an algorithm for the set interface.)