3 ms·

Doesn’t hold water, imo. If dynamic and static typing were really independent concepts, then why are languages only one or the other, never both? I explained my

Doesn’t hold water, imo. If dynamic and static typing were really independent concepts, then why are languages only one or the other, never both? I explained my take on dynamic versus static typing here: https://stackoverflow.com/a/28096079 https://stackoverflow.com/a/28096079 > The primary difference between static and dynamic languages, in my view, is this: in static languages, expressions have types; in dynamic languages, values have types. Read the rest of the answer for more details in the context of Julia, which, as a dynamic language with a sophisticated type system, really crystallizes the distinction.

andrewflnr 7y ago
> in static languages, expressions have types; in dynamic languages, values have types This kind of agrees with OP in practical terms, despite using opposite terminology. A type applied to an expression (syntax) is expressed as a proof about that syntax, and a type of a value at runtime is expressed in code that can safely crash in the face of an ill-typed operation. They both constrain program behavior, but do it with such radically different mechanisms that it's easy to argue they're fundamentally different. It depends on whether "fundamental" should be about mechanism or purpose. Let us know when you've solved that problem. :) Julia's type inference can be seen as finding proofs of the properties of certain expressions and, if it finds them, using them to optimize the dynamic typing code, basically eliminating dead branches for type checks that can't fail. I'm tempted to think of languages with nominal subtyping as being hybrids as well: the base class is the static type, and the runtime class is the dynamic type.
sgeisenh 7y ago
Who said languages were only ever or the other? All languages have some notion of static types and dynamic types. They're most easily bucketed by whether they consider more than one type. C is statically multityped but dynamically unityped. Python is statically unityped but dynamically multityped. Haskell, since it uses lazy evaluation, is statically multityped and dynamically multityped. The main issue with static unityping is that insufficient testing can easily lead to type errors in production (or worse). And static multitypes help static analysis tools reason about code more easily. Introducing a new type that is intended for use in a specific context that can easily be tracked is tremendously useful when programming at scale.
ken 7y ago
As explained in the article: > "The dichotomy between static and dynamic types is somewhat misleading. Most languages, even when they claim to be dynamically typed, have some static typing features. As far as I’m aware, all languages have some dynamic typing features. However, most languages can be characterized as choosing one or the other. Why? Because of the first of the four facts listed above: many of the problems solved by these features overlap, so building in strong versions of both provides little benefit, and significant cost." It's a bit like asking: If electric and gasoline motors are independent concepts, then why are cars only one or the other, not both? Well, some are, to varying degrees. Most aren't, because it adds a lot of complexity. I don't see any inherent contradiction here, nor do I even find the relative unpopularity of hybrid systems terribly surprising.
Tomte 7y ago
But C++ has static and dynamic types, and a C++ programmer needs to understand both. For example, in inherited methods the selection of the method implementation is based on the dynamic type of the (pointer) value, but the selection of the default arguments is based on the static type of the value.
jcelerier 7y ago
> then why are languages only one or the other, never both? what do you mean by that ? multiple statically-typed languages have "var" or "any" types which can be used to go from the static to the dynamic typing world.
- chongli 7y ago
  "Any" types do not imply dynamic typing. Languages like Haskell are purely statically typed yet do not require explicit, concrete types for everything. Type inference is the feature which bridges this gap.
  - jcelerier 7y ago
    type inference and "any" types are completely different. e.g. in C++, auto var = 123; is inference, but std::any var2 = 123; is dynamic typing, because you can do `var2 = "foo bar";` unlike the first case.
vraid 7y ago
Typed racket has both dynamic types and static typechecking. https://docs.racket-lang.org/ts-guide/ https://docs.racket-lang.org/ts-guide/ Your objection doesn't really hold water..
thesz 7y ago
Given algebraic type (as in Haskell - data List a = Nil | Cons a (List a)), you can have static type verification (map :: (a -> b) -> List a -> List b) and dynamic dispatching for situation in concrete part of a program: pairwiseReduce :: (a -> a -> a) -> List a -> List a pairwiseReduce f (Cons a1 (Const a2 as)) = Cons (f a1 a2) (pairwiseReduce f as) pairwiseReduce f as = as We fix the type, but concrete instantiation of a type may vary in run-time, so we pattern-match: the list can have at least two elements (first case) and we reduce them and the rest of the list or it has less than two elements and we leave it as it is. I took my time and read about Julia's type system. It is really the worst from both worlds: it does not allow for tagged unions (like List I declared above), it does not allow for adhoc polymorphism (1+2 gives error for floating type and evaluates for integers), there are no type classes (that adhoc polymorphism thing) and, thus, no good guarantees for whatever substitution for GADTs Julia has. And it also has inheritance which makes type inference exponentially harder in simple cases. So I urge you to take your time and read about Haskell's type system. It really allows you to have static and dynamic types and vary their presence and utility as you see fit.
- KenoFischer 7y ago
  ML Style constructors are not particularly idiomatic, but you can write basically the same thing in Julia: struct Cons{T, S}; head::T; tail::S end pairwiseReduction(f, a::Cons{T, Cons{S, Tail}}) where {T,S,Tail} = Cons(f(a.head, a.tail.head), a.tail.tail) pairwiseReduction(f, a) = a (https://github.com/thautwarm/MLStyle.jl https://github.com/thautwarm/MLStyle.jl if you want the syntax) but that's somewhat beside the point. I think the primary problem here is one of terminology. Take Stefan's quote from the post you're responding to: > The primary difference between static and dynamic languages, in my view, is this: in static languages, expressions have types; in dynamic languages, values have types. There is a clash in terminology here. People coming from a static languages background would use the term "tag" for what dynamic languages people call a type. There isn't really a super good word in the dynamic languages world for what static languages people call a type, and the word type is generally re-used, since the distinction isn't as important (generally there is an embedding of the tags into the type system, so using "type" for both can be sensible). I'm gonna adopt (my best interpretation of) the static languages terminology here for this comment. Some languages have both types and tags. The biggest difference then between static and dynamic languages are which of the two is primarily dispositive (in the sense of determining the semantics of the language). In dynamic languages, the tags are, in static languages the types are. This choice has deep seated implication for the kind of programs that can be written and the behavior of the program. In fact, you sometimes end up in situations where static languages have multiple tag systems (but generally only one type system) and dynamic languages have multiple type systems (but generally only one tag system). In julia, the tag system is primary, but we have a very rich type system that is embedded in the tag system by parametricity and is used for dispatch. This type system is constructed in such a way that the subtyping relationship is induced by tag system (for types T, S, (T <: S iff for all values v s.t. tagof(v) <: T, tagof(v) <: S)) [1]. You basically want to choose a decidable type system that satisfies this constraint, but is at the same time sufficiently expressive to be useful for what people want to do. We also have another, larger type system that is used for inference judgements, but that is generally transparent to the user. It is in principle possible to type check over any of these type static system, but type checking is not part of the semantics of the language. The problem with statements like "Julia's type system does not allow for X", is that it presumes that the type system having some feature is a pre-requisite for having the corresponding functionality. So while Julia's type system does happen have support for unions (and universally qualified unions), the significance of that is for dispatch, not for whether the language can have expressions that can take on values of different tags. In any case, I can assure you that many people working on Julia are well familiar with Haskell's type system. Hopefully I was able to convince you that there is at least something interesting about the way Julia's type system works. [1] I should credit the Northeastern PL group for the term "tag-based semantic subtyping" here to describe this notion (https://github.com/julbinb/ftfjp-2019/blob/master/paper/minijl-ftfjp2019.pdf https://github.com/julbinb/ftfjp-2019/blob/master/paper/mini...).

andrewflnr 7y ago

> in static languages, expressions have types; in dynamic languages, values have types This kind of agrees with OP in practical terms, despite using opposite terminology. A type applied to an expression (syntax) is expressed as a proof about that syntax, and a type of a value at runtime is expressed in code that can safely crash in the face of an ill-typed operation. They both constrain program behavior, but do it with such radically different mechanisms that it's easy to argue they're fundamentally different. It depends on whether "fundamental" should be about mechanism or purpose. Let us know when you've solved that problem. :) Julia's type inference can be seen as finding proofs of the properties of certain expressions and, if it finds them, using them to optimize the dynamic typing code, basically eliminating dead branches for type checks that can't fail. I'm tempted to think of languages with nominal subtyping as being hybrids as well: the base class is the static type, and the runtime class is the dynamic type.

sgeisenh 7y ago

Who said languages were only ever or the other? All languages have some notion of static types and dynamic types. They're most easily bucketed by whether they consider more than one type. C is statically multityped but dynamically unityped. Python is statically unityped but dynamically multityped. Haskell, since it uses lazy evaluation, is statically multityped and dynamically multityped. The main issue with static unityping is that insufficient testing can easily lead to type errors in production (or worse). And static multitypes help static analysis tools reason about code more easily. Introducing a new type that is intended for use in a specific context that can easily be tracked is tremendously useful when programming at scale.

ken 7y ago

As explained in the article: > "The dichotomy between static and dynamic types is somewhat misleading. Most languages, even when they claim to be dynamically typed, have some static typing features. As far as I’m aware, all languages have some dynamic typing features. However, most languages can be characterized as choosing one or the other. Why? Because of the first of the four facts listed above: many of the problems solved by these features overlap, so building in strong versions of both provides little benefit, and significant cost." It's a bit like asking: If electric and gasoline motors are independent concepts, then why are cars only one or the other, not both? Well, some are, to varying degrees. Most aren't, because it adds a lot of complexity. I don't see any inherent contradiction here, nor do I even find the relative unpopularity of hybrid systems terribly surprising.

Tomte 7y ago

But C++ has static and dynamic types, and a C++ programmer needs to understand both. For example, in inherited methods the selection of the method implementation is based on the dynamic type of the (pointer) value, but the selection of the default arguments is based on the static type of the value.

jcelerier 7y ago

> then why are languages only one or the other, never both? what do you mean by that ? multiple statically-typed languages have "var" or "any" types which can be used to go from the static to the dynamic typing world.

chongli 7y ago
"Any" types do not imply dynamic typing. Languages like Haskell are purely statically typed yet do not require explicit, concrete types for everything. Type inference is the feature which bridges this gap.
- jcelerier 7y ago
  type inference and "any" types are completely different. e.g. in C++, auto var = 123; is inference, but std::any var2 = 123; is dynamic typing, because you can do `var2 = "foo bar";` unlike the first case.

vraid 7y ago

Typed racket has both dynamic types and static typechecking. https://docs.racket-lang.org/ts-guide/ https://docs.racket-lang.org/ts-guide/ Your objection doesn't really hold water..

thesz 7y ago

Given algebraic type (as in Haskell - data List a = Nil | Cons a (List a)), you can have static type verification (map :: (a -> b) -> List a -> List b) and dynamic dispatching for situation in concrete part of a program: pairwiseReduce :: (a -> a -> a) -> List a -> List a pairwiseReduce f (Cons a1 (Const a2 as)) = Cons (f a1 a2) (pairwiseReduce f as) pairwiseReduce f as = as We fix the type, but concrete instantiation of a type may vary in run-time, so we pattern-match: the list can have at least two elements (first case) and we reduce them and the rest of the list or it has less than two elements and we leave it as it is. I took my time and read about Julia's type system. It is really the worst from both worlds: it does not allow for tagged unions (like List I declared above), it does not allow for adhoc polymorphism (1+2 gives error for floating type and evaluates for integers), there are no type classes (that adhoc polymorphism thing) and, thus, no good guarantees for whatever substitution for GADTs Julia has. And it also has inheritance which makes type inference exponentially harder in simple cases. So I urge you to take your time and read about Haskell's type system. It really allows you to have static and dynamic types and vary their presence and utility as you see fit.

KenoFischer 7y ago
ML Style constructors are not particularly idiomatic, but you can write basically the same thing in Julia: struct Cons{T, S}; head::T; tail::S end pairwiseReduction(f, a::Cons{T, Cons{S, Tail}}) where {T,S,Tail} = Cons(f(a.head, a.tail.head), a.tail.tail) pairwiseReduction(f, a) = a (https://github.com/thautwarm/MLStyle.jl https://github.com/thautwarm/MLStyle.jl if you want the syntax) but that's somewhat beside the point. I think the primary problem here is one of terminology. Take Stefan's quote from the post you're responding to: > The primary difference between static and dynamic languages, in my view, is this: in static languages, expressions have types; in dynamic languages, values have types. There is a clash in terminology here. People coming from a static languages background would use the term "tag" for what dynamic languages people call a type. There isn't really a super good word in the dynamic languages world for what static languages people call a type, and the word type is generally re-used, since the distinction isn't as important (generally there is an embedding of the tags into the type system, so using "type" for both can be sensible). I'm gonna adopt (my best interpretation of) the static languages terminology here for this comment. Some languages have both types and tags. The biggest difference then between static and dynamic languages are which of the two is primarily dispositive (in the sense of determining the semantics of the language). In dynamic languages, the tags are, in static languages the types are. This choice has deep seated implication for the kind of programs that can be written and the behavior of the program. In fact, you sometimes end up in situations where static languages have multiple tag systems (but generally only one type system) and dynamic languages have multiple type systems (but generally only one tag system). In julia, the tag system is primary, but we have a very rich type system that is embedded in the tag system by parametricity and is used for dispatch. This type system is constructed in such a way that the subtyping relationship is induced by tag system (for types T, S, (T <: S iff for all values v s.t. tagof(v) <: T, tagof(v) <: S)) [1]. You basically want to choose a decidable type system that satisfies this constraint, but is at the same time sufficiently expressive to be useful for what people want to do. We also have another, larger type system that is used for inference judgements, but that is generally transparent to the user. It is in principle possible to type check over any of these type static system, but type checking is not part of the semantics of the language. The problem with statements like "Julia's type system does not allow for X", is that it presumes that the type system having some feature is a pre-requisite for having the corresponding functionality. So while Julia's type system does happen have support for unions (and universally qualified unions), the significance of that is for dispatch, not for whether the language can have expressions that can take on values of different tags. In any case, I can assure you that many people working on Julia are well familiar with Haskell's type system. Hopefully I was able to convince you that there is at least something interesting about the way Julia's type system works. [1] I should credit the Northeastern PL group for the term "tag-based semantic subtyping" here to describe this notion (https://github.com/julbinb/ftfjp-2019/blob/master/paper/minijl-ftfjp2019.pdf https://github.com/julbinb/ftfjp-2019/blob/master/paper/mini...).