3 ms·

Is this type-system guaranteed to be sound? (Does type checking ensure no runtime type bugs?). Also, can it infer all the types if none of the types are actuall

Is this type-system guaranteed to be sound? (Does type checking ensure no runtime type bugs?). Also, can it infer all the types if none of the types are actually annotated? Also, what is the novelty about this new type system?

weatherlight 3y ago
Yes. it's guaranteed to be sound. As per what makes it unique, from the paper: We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching CDuce programming language: https://www.cduce.org https://www.cduce.org
- tannhaeuser 3y ago
  I had to double-check that, knowing CDuce as an XML-oriented language from when XML was hip around almost twenty years ago - and indeed it's that language for manipulating XML. It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall and weren't convincing from a practical PoV. But what do I know - after all, adding types on top of a language that isn't statically typed seems like a pointless exercise to me when there are plenty statically typed languages. I guess it might make sense for a Python code base that's gotten out of control maybe?
  - bcrosby95 3y ago
    It doesn't make sense for certain kinds of languages. But Elixir and Erlang unique in a way that languages like Python, Ruby, etc. are not. A semi-mainstream BEAM language with static typing would be a huge boon. For those of us who have problems that BEAM fits really well, it's like saying Typescript doesn't matter because other statically typed languages exist. Which is really missing the point.
  - josevalim 3y ago
    > It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall Type inference for set theoretic type systems is expensive and that has not changed. It is not surprising either: inference is harder or undecidable in more expressive type systems. We address this by providing reconstruction based only on patterns, guards, and return types. Other than that, inference is not a major limitation to us, given you don’t need to declare types today anyway.
daxfohl 3y ago
Nothing can infer _all_ types. Or even much of a subset. I was surprised to learn that Hindley Milner can't infer "id" as a function argument, and attempting to extend it to do so results in undecidability: https://stackoverflow.com/a/74869648/171121 https://stackoverflow.com/a/74869648/171121

weatherlight 3y ago

Yes. it's guaranteed to be sound. As per what makes it unique, from the paper: We present a gradual type system for Elixir, based on the framework of semantic subtyping [10, 19]. This framework, developed for and implemented by the CDuce programming language [3, 15], provides a type system centered on the use of settheoretic types (unions, intersections, negations) that satisfy the commutativity and distributivity properties of the corresponding set-theoretic operations [19]. The system is a polymorphic type system with local type inference, that is, functions are explicitly annotated with types that may contain type variables, but their applications do not require explicit instantiations: the system deduces the right instantiations of every type variable. It also features precise typing of pattern matching combined with type narrowing: the types of the capture variables of the pattern and of some variables of the matched expression are refined in the branches to take into account the results of pattern matching CDuce programming language: https://www.cduce.org https://www.cduce.org

tannhaeuser 3y ago
I had to double-check that, knowing CDuce as an XML-oriented language from when XML was hip around almost twenty years ago - and indeed it's that language for manipulating XML. It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall and weren't convincing from a practical PoV. But what do I know - after all, adding types on top of a language that isn't statically typed seems like a pointless exercise to me when there are plenty statically typed languages. I guess it might make sense for a Python code base that's gotten out of control maybe?
- bcrosby95 3y ago
  It doesn't make sense for certain kinds of languages. But Elixir and Erlang unique in a way that languages like Python, Ruby, etc. are not. A semi-mainstream BEAM language with static typing would be a huge boon. For those of us who have problems that BEAM fits really well, it's like saying Typescript doesn't matter because other statically typed languages exist. Which is really missing the point.
- josevalim 3y ago
  > It's been a while but I thought the point was to experiment with static typing of XML transformations, but ultimately type inference complexity results hit a wall Type inference for set theoretic type systems is expensive and that has not changed. It is not surprising either: inference is harder or undecidable in more expressive type systems. We address this by providing reconstruction based only on patterns, guards, and return types. Other than that, inference is not a major limitation to us, given you don’t need to declare types today anyway.

daxfohl 3y ago

Nothing can infer _all_ types. Or even much of a subset. I was surprised to learn that Hindley Milner can't infer "id" as a function argument, and attempting to extend it to do so results in undecidability: https://stackoverflow.com/a/74869648/171121 https://stackoverflow.com/a/74869648/171121