41–49 of 49 posts
Nat = Nat + 1 does end up being meaningful: since ultimately the numbers that fall out (e.g. Bool = 2) end up describing the sizes of sets, an interpretation of Nat is some infinite cardinal (aleph-null), which is the size of the set of natural numbers.
Earlier quoted context omitted.
When the Bottom type is included in a language it usually exhibits sub typing behavior. That can be expressed in Haskell, too: {-# LANGUAGE RankNTypes #-} type Bottom = forall a. a -- zero inhabitants f :: Bottom -> a f x = x That passes the type checker just fine.
> That passes the type checker just fine. I think you are running into some weird haskellisms with your Bottom-type. The normal way of defining that in haskell is using the "EmptyDataDecls" pragma, like this: {-# LANGUAGE EmptyDataDecls #-} data Empty g :: Empty -> a g x = x Which doesn't pass the type checker. (From a theoretic standpoint, I would have thought your Bottom was a essentially a type-level identity func…
'forall a. a' is just how you define the bottom type in System F, which Haskell is somewhat based on. As a type it describes that a term of that type can just conjure a value of any type out of thin air, which is obviously nonsense. That what makes it the bottom type.
The sub typing behavior associated with that is just the normal subsumption rule of polymorphic functions. The same reason why you can pass a function of type 'forall a. a -> a' to something expecting a function of type 'Int -> Int'. The types don't 'match' directly, but they do under the subsumption rule.
Earlier quoted context omitted.
> That passes the type checker just fine. I think you are running into some weird haskellisms with your Bottom-type. The normal way of defining that in haskell is using the "EmptyDataDecls" pragma, like this: {-# LANGUAGE EmptyDataDecls #-} data Empty g :: Empty -> a g x = x Which doesn't pass the type checker. (From a theoretic standpoint, I would have thought your Bottom was a essentially a type-level identity func…
Again, languages with a built in bottom usually have sub typing behavior that makes bottom a subtype of everything (so you can give a value of type bottom to everything). 'forall a. a' is just how you define the bottom type in System F, which Haskell is somewhat based on. As a type it describes that a term of that type can just conjure a value of any type out of thin air, which is obviously nonsense. That what makes…
With "forall a. a" I was coming from the persepctive of intuisionistic type theory where the usual parametric polymorphism just get subsumed by Π-types and universal quantification is usually represented with Π-types, so you would have:
forall a.a (Universal Quantification)
Π(a : Type) a (Π-type)
(a : Type) -> a (Agda-notation)
==> a -> a (Π-type as regular function type)
Earlier quoted context omitted.
The "should be able to just return its argument" part is wrong; the types pretty clearly don't match, yeah? It is true that there is a unique function of type `Void -> a` for each `a`, but that isn't it.
When the Bottom type is included in a language it usually exhibits sub typing behavior. That can be expressed in Haskell, too: {-# LANGUAGE RankNTypes #-} type Bottom = forall a. a -- zero inhabitants f :: Bottom -> a f x = x That passes the type checker just fine.
That's fun and a bit surprising, but maybe it shouldn't be. I'm reminded that Dana Scott with Christopher Strachey showed that by using lattices or complete partial orders with a bit of topology to model graphs of possible computations of a program you could, just as in analysis, define least upper and lower bounds and a notion of continuity to derive a construction of limit for a computation which is analogous to a…
[1] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.49....
Earlier quoted context omitted.
Another interesting area of program semantics that hasn’t seen much attention afaik is in the design of languages whose programs form some algebraic structure. My area of research is concatenative programming, where concatenation of two programs denotes the composition of those programs, and the empty program is the identity function (on the “program state”, which is usually a stack). That means that the syntax and s…
Oh neat! (I'm working on using Joy in a practical way, I had an implementation in Python but it turns out Prolog is more conducive: https://osdn.net/projects/joypy/scm/hg/Joypy/blobs/tip/thun/... ) > Unfortunately, it was that “nontrivial” aspect that I could never get past. The language always ended up insufficiently powerful to express anything of interest, its algebraic structure was trivial (e.g. there’s only one…
Well, I didn’t have the skills to actually prove the negative then, I was just never able to find a positive example. Still not convinced that it’s impossible, if I ever get back to it, or someone wants to pick it up as a problem to tinker with.
Earlier quoted context omitted.
Another interesting area of program semantics that hasn’t seen much attention afaik is in the design of languages whose programs form some algebraic structure. My area of research is concatenative programming, where concatenation of two programs denotes the composition of those programs, and the empty program is the identity function (on the “program state”, which is usually a stack). That means that the syntax and s…
This algebraic approach to program semantics is basically how categorical semantics works. The syntactic equational theory of the simply typed lambda calculus with pairs, for example, is that of the "free" cartesian closed category. It can be mapped (in a way that respects the cartesian closed structure) into any cartesian closed category, giving you a semantics. A monoid can be seen as a one-object category (the mon…
Maybe you can offer some insight if I tell you that the quotation syntax “[ … ]” in a concatenative language corresponds to lambda abstraction:
e : a
---------------------
[ e ] : ∀s. s → s × a
quote : ∀sa. s × a → s × (∀t. t → t × a)
compose : ∀rstu. r × (s → t) × (t → u) → r × (s → u)
swap : ∀sab. s × a × b → s × b × a
drop : ∀sa. s × a → s
dup : ∀sa. s × a → s × a × a
quote : ∀sa. s × a → s × (∀t. t → t × a)
apply : ∀st. s × (s → t) → t
The first three correspond to the standard B, C, K, and W combinators from combinatory logic, which give you all the substructural rules from logic—swapping is exchange, dropping is weakening, and copying is contraction. Without swap/drop/dup, it’s equivalent to ordered linear lambda calculus, which can be interpreted in any category (since it’s just B and I); what are the categorical equivalents of linear (BC), affine (BCK), ordered (BKW), and relevant (BCW) logics?
If you like this you'll want to look at "semiring programming" (just search on that phrase) and Categorical Programming, e.g.: "Compiling to categories" Conal Elliott http://conal.net/papers/compiling-to-categories/