4 ms·

To those that know more than I: my understanding before this article was that the only "type-safe" languages were or like Haskell, OCaml, Idris, Agda, etc... I

by Ixiaus 12y ago

To those that know more than I: my understanding before this article was that the only "type-safe" languages were or like Haskell, OCaml, Idris, Agda, etc... If that's not the case is "type-safe, pure, and functional" a good epithet to extend, say, Haskell's "type-safe" tag with many of its other features that weave with the type system well?

gipp 12y ago
"Type-safe" as used in the FP community tends to be a much stronger claim than what's described in this post. At the very least, throwing a runtime exception is considered "going wrong" in the Haskell community, and this post keeps throwing out examples of runtime exceptions as avoiding "going wrong".
tel 12y ago
"Type safe" is both a marketing line and a technical definition. As a technical definition, many languages are type safe (including, say, Ruby) but they achieve this by having very low meaning to their (static) types. Typically, the marketing definition means "type safe and expressively typed" which outlaws trivial type systems and their trivial type safety.
- Ixiaus 12y ago
  I read your blog post, thanks for the longer description :)
mnarayan01 12y ago
I believe Haskell would be considered have "strong static typing". Unfortunately, "strong" in this context is less precise than one might like: both Haskell and Java are generally considered "strongly typed", but Java allows e.g. type casting in a way that will not be statically type checked. Haskell also uses type inference rather than requiring type declarations, but that is not _directly_ related.
- tel 12y ago
  Type casting has to be modeled (more or less) as (a) upcasting only (b) a failure of type safety, or (b) an admission that the type system is entirely vacuous.
  - AnimalMuppet 12y ago
    No, you can have downcasting that is checked for validity at runtime, a la Java (or C++ with RTTI). This is not a failure of type safety, since only valid casts will be performed. It's not vacuous, either - it's not just one big type.
    - tel 12y ago
      What happens when a cast is invalid? You have type-safe casts in Haskell, for instance, where the failure is reflected at runtime. cast :: (Typeable a, Typeable b) => a -> Maybe b Those are alright.
      - AnimalMuppet 12y ago
        In Java, IIRC, the cast fails with a ClassCastException. That seems to me to be "failure is reflected at runtime". In C++ with RTTI, IIRC it returns null. That's also "failure at runtime" (of a sort), but you have to check it.
        jeorgun 12y ago
        RTTI returns nullptr when casting a pointer, but it does throw an exception when casting references. Both of these behaviors are well-defined, although the first is kind of questionable.
- sparkie 12y ago
  Haskell also allows casting in a way that defeats static type checking - `unsafeCoerce`
- marcosdumay 12y ago

by Ixiaus 12y ago

gipp 12y ago

"Type-safe" as used in the FP community tends to be a much stronger claim than what's described in this post. At the very least, throwing a runtime exception is considered "going wrong" in the Haskell community, and this post keeps throwing out examples of runtime exceptions as avoiding "going wrong".

tel 12y ago

"Type safe" is both a marketing line and a technical definition. As a technical definition, many languages are type safe (including, say, Ruby) but they achieve this by having very low meaning to their (static) types. Typically, the marketing definition means "type safe and expressively typed" which outlaws trivial type systems and their trivial type safety.

Ixiaus 12y ago
I read your blog post, thanks for the longer description :)

mnarayan01 12y ago

I believe Haskell would be considered have "strong static typing". Unfortunately, "strong" in this context is less precise than one might like: both Haskell and Java are generally considered "strongly typed", but Java allows e.g. type casting in a way that will not be statically type checked. Haskell also uses type inference rather than requiring type declarations, but that is not _directly_ related.

tel 12y ago
Type casting has to be modeled (more or less) as (a) upcasting only (b) a failure of type safety, or (b) an admission that the type system is entirely vacuous.
- AnimalMuppet 12y ago
  No, you can have downcasting that is checked for validity at runtime, a la Java (or C++ with RTTI). This is not a failure of type safety, since only valid casts will be performed. It's not vacuous, either - it's not just one big type.
  - tel 12y ago
    What happens when a cast is invalid? You have type-safe casts in Haskell, for instance, where the failure is reflected at runtime. cast :: (Typeable a, Typeable b) => a -> Maybe b Those are alright.
    - AnimalMuppet 12y ago
      In Java, IIRC, the cast fails with a ClassCastException. That seems to me to be "failure is reflected at runtime". In C++ with RTTI, IIRC it returns null. That's also "failure at runtime" (of a sort), but you have to check it.
      - jeorgun 12y ago
        RTTI returns nullptr when casting a pointer, but it does throw an exception when casting references. Both of these behaviors are well-defined, although the first is kind of questionable.
sparkie 12y ago
Haskell also allows casting in a way that defeats static type checking - `unsafeCoerce`
marcosdumay 12y ago