There was a pretty interesting addition to the Go generics discussion. I don't know if this is quite FP, but it does involve Philip Wadler, and type systems, so I thought it might interest people here.
One interesting result of this design is a unique kind of generic data structures. Because Go does not have ADTs it might seem like you can't ergonomically emulate types like Maybe and List but actually you can in a sort of way with this generics proposal. What you can do is specify an interface, and then implement the constructors as separate types that implement that interface. for example you could have a struct Nil that contains no members, and a struct Cons that contains a member of type a, and a List a where List is an interface. One of the interesting outgrowths of this combined with Go's structural typing is that you define a bunch of types for free. For example I could create another struct that implements list called append, and it contains 2 List a. In Haskell if I have some code that uses lists and I realize I want to do something that uses a lot of appends, and that I should probably switch to a DList, it becomes a bit of a hassle. But in this version of Go it's not a problem.
In the talk he mentions the possibility of Haskell learning something from Go here -- a way out of the nominal structure of type classes would be my guess.
@Torsten Schmits that two types are equivalent or sub-types of one another by explicit declarations; in contrast to structural where a type that has similar structure can be considered a sub-type or equivalent to another.
I don't recall him spelling it out in the talk but I assume he meant that Go does something useful here that would enable Haskell to shuffle around the type class hierarchy without forcing everyone to update their code.
And how if we did this change in Haskell we could have avoided forcing everyone to update their code to handle the new hierarchy. Does that make sense?
It's not so much a way out of problems caused by typeclasses (although there's that too) but out of the more fundamental problem caused by generative type and data constructors (e.g. in the case of sum types). Every time you create a new data type in Haskell it can't hope to be more closely related to another type than via an explicit isomorphism that pollutes all your other code. In structural typing, types can end up being strictly equivalent
in more natural language it means that it is impossible to exactly unify the type constructors introduced by two distinct data/newtype declarations by applying some arguments to each, even though it is very often the case that applying some type arguments to each gives you a pair of isomorphic types
There was a pretty interesting addition to the Go generics discussion. I don't know if this is quite FP, but it does involve Philip Wadler, and type systems, so I thought it might interest people here.
the paper:
https://arxiv.org/abs/2005.11710
a talk on it by Philip Wadler:
YouTube - Phil Wadler: Featherweight Go
One interesting result of this design is a unique kind of generic data structures. Because Go does not have ADTs it might seem like you can't ergonomically emulate types like
MaybeandListbut actually you can in a sort of way with this generics proposal. What you can do is specify an interface, and then implement the constructors as separate types that implement that interface. for example you could have a struct Nil that contains no members, and a struct Cons that contains a member of type a, and a List a where List is an interface. One of the interesting outgrowths of this combined with Go's structural typing is that you define a bunch of types for free. For example I could create another struct that implements list called append, and it contains 2 List a. In Haskell if I have some code that uses lists and I realize I want to do something that uses a lot of appends, and that I should probably switch to a DList, it becomes a bit of a hassle. But in this version of Go it's not a problem.In the talk he mentions the possibility of Haskell learning something from Go here -- a way out of the nominal structure of type classes would be my guess.
@James King what does "nominal structure" mean?
@Torsten Schmits that two types are equivalent or sub-types of one another by explicit declarations; in contrast to structural where a type that has similar structure can be considered a sub-type or equivalent to another.
I don't recall him spelling it out in the talk but I assume he meant that Go does something useful here that would enable Haskell to shuffle around the type class hierarchy without forcing everyone to update their code.
would that be a new language feature that allows specifying type class relationship with something other than dependency constraints?
or is this about the equivalence of the types that inhabit type classes?
Or maybe class
Generics :big_smile:ClassKinds?He wasn't specific -- if you want to know more I recommend watching the talk :smiley:
Or maybe send him an email and let us know what he says.
:slight_smile:
my question was more about your explanation than what was hinted at in the talk
In that case to your first question, I think that might be what he was hinting at.
Because he was mostly talking about type classes and specifically the change of monad's super classes
And how if we did this change in Haskell we could have avoided forcing everyone to update their code to handle the new hierarchy. Does that make sense?
yes, interesting. thanks!
It's not so much a way out of problems caused by typeclasses (although there's that too) but out of the more fundamental problem caused by generative type and data constructors (e.g. in the case of sum types). Every time you create a new data type in Haskell it can't hope to be more closely related to another type than via an explicit isomorphism that pollutes all your other code. In structural typing, types can end up being strictly equivalent
e.g.
Compose (Const Foo) Barcan actually be preciselyConst Foo, you don't need to manage an isomorphism between those two everywhereor lists can actually be precisely the fixpoint of
\a r -> Maybe (a, r), instead of only being isomorphic to it@Asad Saeeduddin what does "generative" mean here?
@Torsten Schmits There's a good definition of it in this paper: https://www.microsoft.com/en-us/research/uploads/prod/2019/03/unsaturated-type-families-icfp-2019.pdf
but to quote it
where
~is equality of types and=>is implicationin more natural language it means that it is impossible to exactly unify the type constructors introduced by two distinct
data/newtypedeclarations by applying some arguments to each, even though it is very often the case that applying some type arguments to each gives you a pair of isomorphic typesif
aandbdon't matter for the equality, are they phantoms?that is, if they don't need to be equal
ah, no, it's a condition, so they do matter
Yes, they may or may not be equal. It's simply saying that no possible
aandbexist such thatf a ~ g bunlessf ~ g.https://blog.golang.org/generics-next-step you can now try it out for yourself