The algebra and calculus of algebraic data types • Hacker News Board

Re: The algebra and calculus of algebraic data types

#31

Post by rntz » Sun, Sep 09, 2018, 9:37 AM UTC

evincarofautumn wrote: post #25

vajrabum wrote: post #13

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…

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 monoid elements are the morphisms on that object, and the monoid operator is morphism composition), so perhaps concatenative languages have categorical semantics too. (Although it seems like the semantics of "quote", or whatever [ foo bar baz ] is in forth, might make things a little interesting - ie. require more structure than a monoid homomorphism. I expect you really want cartesian closed categories, and quote is probably curry or apply.)

Re: The algebra and calculus of algebraic data types

#32

Post by tpush » Sun, Sep 09, 2018, 10:26 AM UTC

matt-noonan wrote: post #24

tpush wrote: post #8

Earlier quoted context omitted.

Since one can prove anything if you're assuming nonsense, a function of the type 'Void -> a' should be able to just return its argument. And assuming the theory is consistent(so no infinite loops etc.) this is the only instance of that function, so the cardinality is 1.

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.

Re: The algebra and calculus of algebraic data types

#33

Post by vignesh_m » Sun, Sep 09, 2018, 10:29 AM UTC

This is almost identical to the study of combinatorial species (https://en.wikipedia.org/wiki/Combinatorial_species)

Re: The algebra and calculus of algebraic data types

#34

Post by abecedarius » Sun, Sep 09, 2018, 11:11 AM UTC

benrbray wrote: post #29

I once tried to take the Taylor series idea further and define the "cosine" of a type as the Taylor expansion of cos(x), but didn't get anywhere with it. Can you do anything else weird with ADTs?

Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term.

What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to be 2^x -- that is, x -> Bool -- because it's isomorphic to the characteristic function of a set, and a function type is an exponential (https://bartoszmilewski.com/2015/03/13/function-types/). But 2^x differs from exp(x) by a constant factor. So I seem to be messing with surface-level analogies without real understanding.

Re: The algebra and calculus of algebraic data types

#35

Post by etatoby » Sun, Sep 09, 2018, 1:01 PM UTC

abecedarius wrote: post #34

benrbray wrote: post #29

I once tried to take the Taylor series idea further and define the "cosine" of a type as the Taylor expansion of cos(x), but didn't get anywhere with it. Can you do anything else weird with ADTs?

Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to…

You're comparing unordered lists of unlimited length with subsets.

To define a subset of x, you simply choose whether any element is present or not:

type Set x = x → Bool

Cardinality: 2^x

Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be surprised if it was not possible, or if the expansion turned out to have a strange cardinality such as e^x

Re: The algebra and calculus of algebraic data types

#36

Post by abecedarius » Sun, Sep 09, 2018, 2:48 PM UTC

etatoby wrote: post #35

abecedarius wrote: post #34

Earlier quoted context omitted.

Huh. Thinking about this example I'm confused, because the power series for exp(x) looks like the type for unordered lists of x: e.g. the term for lists of length three is x^3, and if you ignore order you get x^3/3!. The cosine is almost the same as the even terms of this series, but with a minus sign on every other term. What confuses me (besides what to make of the minus sign) is that the type of sets of x ought to…

You're comparing unordered lists of unlimited length with subsets. To define a subset of x, you simply choose whether any element is present or not: type Set x = x → Bool Cardinality: 2^x Defining an unordered list (of unlimited length, with possible repetitions) with algebraic data types is harder, if at all possible. Especially when you consider what "unordered" should mean in the face of repetitions. I wouldn't be…

Thanks, I forgot about repetitions of the same element. How could I miss that?

Re: The algebra and calculus of algebraic data types

#37

Post by rfw » Sun, Sep 09, 2018, 6:09 PM UTC

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.

Re: The algebra and calculus of algebraic data types

#38

Post by carapace » Sun, Sep 09, 2018, 9:42 PM UTC

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/

Re: The algebra and calculus of algebraic data types

#39

Post by carapace » Sun, Sep 09, 2018, 9:46 PM UTC

evincarofautumn wrote: post #25

vajrabum wrote: post #13

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…

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 program), or it ended up having a weaker structure (e.g. an idempotent semiring). Chris Pressey also worked on this concept a bunch around 2007, and produced some results like Cabra² and Burro³, but ran into similar dead ends like Potro⁴.

Maybe that in itself is an important result?

Re: The algebra and calculus of algebraic data types

#40

Post by joel_ms » Mon, Sep 10, 2018, 5:49 AM UTC

tpush wrote: post #32

matt-noonan wrote: post #24

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 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 function..)