Better sum types for go

[Axel Wagner]

Hey gophers,

I had a thought to me and as far as I'm aware, it's a new one (though, forgive me if it isn't), about how to prevent re-implementations of an interface:

https://play.golang.org/p/0B-fmVhhZa

Let me know, what you think :)

Axel

[as....@gmail.com]

But why go through such length to prevent implementation of interface? Interface demands satisfaction! 

[Jan Mercl]

On Sun, Jun 12, 2016 at 5:57 PM <as....@gmail.com> wrote:

> But why go through such length to prevent implementation of interface? Interface demands satisfaction! 

https://youtu.be/poXvMBhjSWk </troll>

--

-j

[Axel Wagner]

To approximate sum-types.

Adding sum-types have been repeatedly proposed and where repeatedly rejected, because a) yes, they are useful, but b) their usefulness doesn't justify the cost of adding complexity of the language, especially as c) you can approximate them with interfaces (and I agree on all three counts). What this is trying to do, is to add a little bit more safety to c, for use cases where sum types are a good solution, but are lacking from go.

So this is a conscious break with what interfaces are intended for, they are only used as a bodge to approximate a different concept. When you want to use sum-types, you can't usually use an interface because they are a behavioral type-definition and 1) you want to express a possible set of types, but 2) you want it to be closed and 3) the members of the set isn't defined by shared behavior.

A thing that sum types often are used for are nodes in an AST, for example go/ast does the same kind of approximation of sum-types [0] (the kind that I described in the first half of that post). What I describe in the second half is a way to make this a little bit safer, for use cases where you do want to use the concept but only have the approximation via interfaces. It's a demonstration that you can, effectively, make the set of types expressed by a set to be closed, so fulfilling 2 from above, which, formerly (to the best of my knowledge, I am happy to be corrected :) ) was thought to not be possible.

[0] https://golang.org/src/go/ast/ast.go#41

--
You received this message because you are subscribed to the Google Groups "golang-nuts" group.
To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[as....@gmail.com]

I use go/ast package mildly to moderately, but the lack of safety between ast.{Node,Expr,...} etc hasn't been a problem yet. I'm actually not sure what safety means in this case. What you are describing fits closest to the concept of a discriminated union, which I thought was nice in Limbo (pick) but didn't really miss too much after using Go more frequently, and I can see why they weren't included in the language.

You could also construct something like this, but its not really a union in the classical sense.

package main

import "fmt"

type(

  A struct{}

  B struct{}

  C struct{}

  Union struct{

    A *A

    B *B

    C *C

  }

)

func main(){

a := &Union{A: &A{}}

fmt.Println(a)

}

[Axel Wagner]

On Sun, Jun 12, 2016 at 7:58 PM, <as....@gmail.com> wrote:

I use go/ast package mildly to moderately, but the lack of safety between ast.{Node,Expr,...} etc hasn't been a problem yet.

I am not even disagreeing with you here. But there are people who clearly perceive it as a problem, otherwise there wouldn't be repeated questions and proposals about this. And it doesn't really have a cost associated to it, in comparison to what go/ast already does.

 

I'm actually not sure what safety means in this case.

Less opportunity for people to make mistakes that make a program panic.

 

What you are describing fits closest to the concept of a discriminated union

Yes, that's another word for sum type, AFAIK.

 

, which I thought was nice in Limbo (pick) but didn't really miss too much after using Go more frequently, and I can see why they weren't included in the language.

As I said before: I can see that too. But, as I said before, one large part of that is that there already is a good enough approximation of it via interfaces. This makes the approximation a tiny bit better :)

But, I'm not even arguing for people to really *do* try to use sums. I just say if they do feel the need and they do want it closed, this is a way to achieve it with what's already in the language.

[Jesper Louis Andersen]

On Sun, Jun 12, 2016 at 11:09 PM, 'Axel Wagner' via golang-nuts <golan...@googlegroups.com> wrote:

I'm actually not sure what safety means in this case.

Less opportunity for people to make mistakes that make a program panic.

 

In the context of types, it often means that the system has two properties:

progress - which roughly means that any well-typed program fragment either is a value (i.e., fully reduced) or can take a step (towards full reduction).

preservation - which informally means that if a program has type T before reduction, it preserves that type throughout the computation. I.e., it is not possible to switch the type of a program in the middle of the computation.

Together, they form a protective barrier for a well typed program in that it cannot go wrong with a type error. Typical things which destroys this property are stuff like type casts (C-style), since preservation is thwarted.

If I have a function from AST to Stmt, say, then if I'm able to return something of type Expr, say, it isn't type safe in the above sense. It switches the return type from an Stmt to an Expr.

You can argue that sum types should not be added to a language[0], but they are absolutely indispensable as a tool for understanding program semantics. The sum type is a generalization of a lot of patterns you see in typical "mainstream" languages: exceptions, the Go error type, dynamic dispatch (i.e., OOP), and "dynamic typing" are all concepts enjoying an embedding in the fabric of sum types. So the study of these subjects are greatly helped along if you cast them as sum types in your semantic logic.

[0] Given that a language has products, i.e., structs/records, I find it quite natural to add it's logical dual, sums, as well. If you think about it, a product/struct correspond to "type X AND type Y AND ...", logical conjunction, whereas the sum is "type X OR type Y OR ..." which is logical disjunction. A logic with only one side is severely limited in expression. So this is one of the places I politely disagree with the Go stance. Once sums are inside the language, you can write optimization passes in the compiler for them, which is a necessity; otherwise you end up wasting allocations you could have avoided in the first place.

--

J.

[as....@gmail.com]

It would be interesting to see what real world benefits such an addition would have. Discriminated unions need a discriminant. I've seen a few languages that implement this, albeit hideously. What research or other literature can you recommend on the topic of type theory?

[Michael Jones]

The position of the language designers:

https://golang.org/doc/faq#variant_types

My personal position is that discriminated unions would be good. Discussed in 2012:

https://groups.google.com/forum/#!searchin/golang-nuts/union/golang-nuts/VZ0rY12nzSM/ZV-4-sQ2R_IJ

[Matt Harden]

+1 for sum types/discriminated unions. We should try to add these to Go, if a good syntax & implementation can be brought forward. Interfaces are not a fully satisfactory alternative.

--

[Jesper Louis Andersen]

On Mon, Jun 13, 2016 at 1:58 AM, <as....@gmail.com> wrote:

What research or other literature can you recommend on the topic of type theory?

Benjamin C. Pierce's "Types and Programming Languages", often abbreviated TAPL, is a classic text on type theory. Working from the semanticists favorite toy language, the Lambda-calculus, Pierce proceeds to add different type-theoretic constructs on top of it one at a time to explain their concepts. Don't let the choice of the lambda-calculus fool you. Once you add references into that language it essentially becomes a basis for imperative programming.

--

J.

[Viktor Kojouharov]

I'm also for such types. There was also an interesting discussion about them here:

https://www.reddit.com/r/golang/comments/46bd5h/ama_we_are_the_go_contributors_ask_us_anything/d03t6ji?context=3

[as....@gmail.com]

Thanks!