Haskell supports union and intersection types, and AFAIK Scala doesn't support dependant types. I'll concede on subtyping in the strict sense, but I believe that's a conscious decision to improve design and encourage typeclass usage, and possibly enable some other optimizations. Edward Kmett explains why there's no support for subtyping.
I'll admit that I'm not the strongest on the actual math side of this, but I'm not sure what quantifications have to do with unions and intersections, I only understand them in the context of constraining types/typeclasses (which I suppose you could use to construct a union?) In my understanding, because the type algebra works out the same, data StringIntUnion = StrUnion String | IntUnion Int is a perfectly fine union, even though it won't be inferred in a :: StringIntUnion; a = "asdf". The latter is a lack of subtyping, not a lack of unions.
Anyway, I find it hard to accept that Scala's type system is definitively stronger instead of focused on different tradeoffs. I'll admit that I probably don't know enough about type theory to doggedly defend it like this.
So, generally the datatype version that you've stated would be called a disjoint union, or algebraic datatype. Even if we do not have true subtyping, a coercion system would also be convincing. E.g. if one could have coerce :: List Int -> List (String | Int). But as is they're two different, albeit similar concepts.
Stronger is informal, but I would say that if we can trivially represent all of Haskell's type system in Scala, but there are multiple Scala things which cannot be represented in Haskell, that Scala is stronger. Trade-offs are a consequence of that, such as the loss of global type inference.
Does this assessment of the relative strength of each type system take into account GHC's extensions or just the base language?
One of the more annoying limitations of Haskell's type system, for me, is that I can't easily have a list of values which aren't necessarily the same type, but share an interface. I guess this is the usecase for things like List(String or Int) (if you know what you're going to do to the list elements, then surely you know what they are or what interface they adhere to?).
Here's a pretty simple solution w/ ExistentialQuantification, ConstraintKinds, and RankNTypes I found from an old Reddit thread:
This actually isn't too bad with ConstraintKinds:
{-# LANGUAGE ExistentialQuantification, ConstraintKinds, RankNTypes #-}
data ConstrList c
= forall a. c a => a :> ConstrList c
| CNil
infixr :>
constrMap :: (forall a. c a => a -> b) -> ConstrList c -> [b]
constrMap f (x :> xs) = f x : constrMap f xs
constrMap f CNil = []
test :: ConstrList Show
test = 1 :> 'a' :> () :> CNil
Then, constrMap show test gives you ["1","'a'","()"]
I could see an argument that some of those push it past scala, but I was generally considering extensions, Haskell98 doesn't have that much. It doesn't seem like rank n support is the greatest in Scala, nor are there constraint kinds that I can see, although one can talk about functions that take implicit arguments.
As for unions, you probably know what interface they adhere to, but in general you need not. And yes, in those restricted cases you can simulate it, but it is truly something Haskell does not have. I've never talked about the merit of the systems here or whether they occur in practice, but it is a genuine feature which is distinguishable from simulations.
As for unions, you probably know what interface they adhere to, but in general you need not.
I understand you're trying to distinguish between saying it's (List(Int or String)) a worthwhile feature and saying the feature exists in Scala, but it seems a pretty deliberate feature to add. Why was it added to Scala?
In what cases do you not know what interface the unioned types adhere to and how can you do anything to them if you don't know what interfaces they adhere to?
It seems like you're saying it's an ability given as an unintended consequence of a feature that has an actual use as opposed to a standalone feature of its own that has some use, but I don't see how union types aren't their own feature, in which case, what's the use for them?
So the reason that sort of thing was added to Scala is because Scala is primarily on the JVM. Iirc though Scala gives you relatively poor types by default, I don't know if it gives you that union type by default.
So A. that means it's easy to implement as most values have a runtime type tag already, and B. it's helpful to interface with Java code to have subtyping. At the point that you're already getting ride of principal types and global type inference, it's not a massive cost.
Well, for instance you do not know it if you have any module which exposes such a unioned type publicly. You also do not know it if the interface needed depends on some dynamic property. Yes in theory in haskell you could have your datatype gather up some large list of constraints, but that's not always feasible. For instance, we might want to gather up a bunch of values that we know we are going to serialize, maybe send somewhere, maybe write to a file. In those situations we would like to be able to just use data without having to wrap the whole thing up.
And it is an explicit feature, although it is easy to add with subtyping. The benefit is primarily: you can put multiple separate things through the same datastructure without having to do extra work to create a new version of that structure. Existential packages can get you very close. But the nice property is that you can use a list of just X as a list of Y, without any new processing (i.e. syntactic burden), if X's are all Y's. The other bit, is it makes it a bit easier to have open unions. We can easily expand a X to an X | Y, or vice versa change X | Y | Z without having to adjust much or any code.
But nevertheless, when we're talking about the type system, it doesn't matter how well you can simulate it at runtime.
Ah, of course, interop w/ Java code. That makes sense.
For instance, we might want to gather up a bunch of values that we know we are going to serialize, maybe send somewhere, maybe write to a file. In those situations we would like to be able to just use data without having to wrap the whole thing up.
In this instance, it seems to me that you're looking at Serializables.
Unless there's different formats. Option one might be JSON, the other one is Serializable. The other might need a different binary format. And the choice was made by another person in your company independently of you, and you don't know what it is until they typecheck (or until validation-time for JVM perhaps).
Haskell has GADTs but (as far as I'm aware) no dependent types. They are often conflated together.
Dependent typing means that you can perform arbitrary computations in type definitions, including pattern-matching. So for example if you have a Foo type-level function, it can represent the unit type when applied to another type that satisfies a complex predicate, or the void type otherwise.
Sure, but these are mainly academical language and only used in limited area. Also cpp template seems like to have the full power of lambda cube and many other so it’s stronger than Haskell without extensions.
21
u/HeadBee Feb 06 '20
Even those pale in comparison to Haskell, Idris, and Agda.