Wouldn't that make countries like the USA and Canada extremely far apart because they are both large countries? The distance you would get is the distance from Hawaii to somewhere on the northeastern edge of Nunavut/Newfoundland/Labrador
265 karma · joined February 1, 2014
Then the inverse-image definition of a continuous function is clearly satisfied by computable functions. A function f : A -> B is continuous if for any semidecidable property O on B, the property { x \in A. f(x) \in O } is semidecidable (since f is a computable function).
There's some very cool ideas here like Hausdorff == Diagonal is closed =~ the equality predicate is co-semidecidable, i.e., you can implement a partial inequality function that always returns true if the inputs are not equal.
See Martín Escardó's work for more details: https://www.cs.bham.ac.uk/~mhe/papers/barbados.pdf
As for why delimited continuations are not more popular, many people find shift/reset a bit difficult to program with. In particular the type systems for them are a bit odd and some variants like prompt/control don't have nice type systems for them. Currently, the closely related notion of (algebraic) effect handlers is quite popular in the functional language design community as something quite similar in expressive power but more intuitive for programming and with very natural typing. The Koka language has a lot of nice introductory resources if you are interested in learning more: https://github.com/koka-lang/koka . There's even a serious proposal for adding something based on these to webassembly: https://github.com/effect-handlers/wasm-effect-handlers .
If you read McBride's paper "Clowns to the Left of Me, Jokers to the Right" (https://www.cis.upenn.edu/~cis39903/static/clowns.pdf) is exactly about systematically deriving the type of defunctionalized stacks for the fold over an ADT. The ordinary derivative is then the special case where you are just mapping a function that doesn't change the type.
As an example, the function type `A -> B` is negative because the function introduction rule
G, x:A |- M : B ---------------- G |- lam x. M : A -> B
is a bijection: the inverse is
G |- N : A -> B ------------------- G , x:A |- N x : B
The beta and eta equations encode exactly the two properties of this being a bijection.
Positive types, like sums/alternatives/coproducts have their elimination rule as their reversible rule, i.e. "pattern matching". So the rule
G , x1 : A1 |- K1 : B G , x2 : A2 |- K2 : B --------------------- G , x : A1 + A1 |- case x of { in1 x1. K1 | n2 x2. K2 }
Has an inverse
G , x : A1 + A2 |- N : B --------------------------- G , x1 : A1 |- N[in1 x1/x] G , x2 : A2 |- N[in2 x2/x]
The reason people say the positive types are "defined in terms of their introduction rules" is that you say "here are all the ways to build a term of this type" (in1 and in2 for sums) and then the elimination rule is exactly "pattern match on all of those possibilities". There is a dual way to think of the negative types which is "here are all the ways to use a term of this type" and the introduction form is a "co-pattern match" where you say "inspect all of the ways I can be used and say what to do in each case".
If you know about category theory then the idea is that some types are defined by representing a functor C -> Set (positives) and others by representing a functor C^op -> Set (negatives).
Variance is I would say is an orthogonal concept, except that the only primitive contravariant type former in lambda calculus is function which is negative.
1. The type theorists/homotopy theorists that are exploring homotopy/cubical type theory as a foundational approach.
2. The objective fact that in general the internal language of a topos (in general) does not validate the law of excluded middle or the axiom of choice. This means that if you prove a result while using constructive logic you can apply it to a broader class of models than classical logic. This viewpoint of logic makes the whole "argument" between constructive and classical logic seem very silly: it's like arguing whether or not it is "true" that groups are abelian. Some are and some aren't!
Intuisionism as in Brouwerian intuitionism with choice sequences etc that disprove LEM is still a niche subject, especially foundationally but is still being explored, with the help of understanding of sheaf models that allow it to be studied from a classical perspective.
But also it's important to note that it's not Typed Racket or Racket in isolation that are slow, but the inter-mingling of the two due to contract overhead.
There's no object X where E/X is pointed sets. If you take the co-slice of a one point set 1\E that would be the category of pointed sets.
The right way to think about E/X is that its objects are "families of sets indexed by X", because a function f : Y -> X defines for each x in X a set f^{-1}(x). If you know about dependent types, this is basically a type dependent on X.
This also says why classical logic can still be useful: if I'm going to use continuations all the time, it's nicer to program with a language that supports them than to explicitly program in CPS. Pick the right language/logic for the task at hand!
A couple comments 1. I would say the primary application is to proving that certain casts (function cast, etc.) are the primary result of the paper. We basically showed that graduality + extensionality determines almost all of the behavior of casts. 2. Exception handling for type errors is actually in direct conflict with graduality. The reason is that the type error is the least element and every term has to be monotone with respect to the type error, so if you catch a type error, to be monotone you have to show that the result you produce is less dynamic than the result you would have produced if there was no exception. This means that if you want to catch type errors you need to have a fancy catch form, or you need to do it at an "extra-linguistic" level, or you can use modal types (think monads) to say that catching a type error is a "reflective" operation and so any code that does it is uses the reflection modality.
Also as a side-note, in my opinion profunctors are an essential component of category theory, and it's really a shame that in intro courses we explain everything in terms of adjunctions, limits, presheaves, etc when profunctors are ultimately simpler. They are unavoidable when you do enriched/internal category theory and they are more directly useful in designing type theories than adjunctions.
> If Newton had known about such functions, he would have never created calculus.
since Newton did use infinitesimals in his reasoning.