12 ms·

What I Want from a Type System (2016)

106 points by grzm 7y ago

foxes 7y ago
Honestly you can nearly write Haskell without specifying type signatures. GHC is very sophisticated. I feel like there have only been a few situations where I actually needed to specify the type. Really the argument shouldn't be about having strict types vs dynamic, it should be about smarter compilers etc. To me, GHC seems to be nearly perfect (also GHCi).
- 87zuhjkas 7y ago
  I agree, GHC has the best type inference that I know of.
- nestorD 7y ago
  Ocaml also standout as a language in which you can omit type definitions (the only exception I ever needed was when deserializing data).
  - aloisdg 7y ago
    In the same vein F# as a descendant of OCaml, opens all of this fot the .Net world.
    - nestorD 7y ago
      F# adds a [] operator to access containers (mostly arrays and dictionnaries) and unifies arithmetic operators (no more +.). While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.
- deleted 7y ago
  [deleted]
- yogthos 7y ago
  HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct. Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety. Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort. [1] https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste...
  - Drup 7y ago
    This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.
    - yogthos 7y ago
      A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...
cjfd 7y ago
I don't agree with this at all. Having the types of every variable written explicitly in the code is important documentation that answers very quickly the question 'what is the type of this thing' without having to look everywhere and anywhere to perhaps find out that it could be any one of three types. If you do not know the type of something you also do not know what operations are available on that thing.
- empath75 7y ago
  Use an IDE
  - wereHamster 7y ago
    I'm not always using an IDE when looking at code. Sometimes I read code directly on GitHub, or repl.it, or codesandbox, or ….
    - Waterluvian 7y ago
      Maybe those can evolve further too. I've always appreciated the advantages of code being legible as plain text files. But maybe it is just a little absurd when language design is shaped to fit the desire not to evolve the storage format and editing interface.
    - azhenley 7y ago
      I agree with your comment. GitHub does seem to be moving towards adding IDE-like features though: https://github.com/github/semantic https://github.com/github/semantic
- pjc50 7y ago
  It looks like there's two very different styles going on here. Most of us are used to the OO-type approach (Java, C#) where the operations are "inside" the object and defined on it. This article is coming from a very different place where the operations are "outside" the typed things, which are more like structs, and the programmer can write any operation that takes structs which have the right fields. The author doesn't make any comment on dispatch let alone multiple dispatch. They appear to be writing for the kind of quasi-schema'd information bureaucracy that's very important outside of SV. Lots of data in XML that never quite lines up with an object model. The Haskellite approach would also say that "what operations are available on that thing" is the wrong way round; you define your operation, and the type signature tells you what kind of things will work with it.
yakshaving_jgt 7y ago
…Sounds like he just wants row polymorphism, no?
karmakaze 7y ago
> Value types in structures would need to be nominal The reasoning behind wanting this is good. It can however be satisfied differently. I find structural typing to be more convenient where I have the ability to define a type for another that is not considered to be equivalent. A good example is how an int can be defined into different types with conversions in Go. If we were to follow through with nominal typing we would need transforms to rename the same structures when working through abstractions that make sense having different names.
thesz 7y ago
This is the case when someone didn't completed his homework. Most of things he requested are possible with HList in Haskell. A library, nonetheless. From 2008, I believe. PS Structural subtyping is tricky: https://pdfs.semanticscholar.org/ff6f/1c49ff00efa483807fae71ef2a0f2baf6a04.pdf https://pdfs.semanticscholar.org/ff6f/1c49ff00efa483807fae71... It took quarter of century to get it right. Most probably the author of gist just don't get it's trickyness yet.
- gpderetta 7y ago
  in fact, most of those things are possible in c++ of all places.
  - ken 7y ago
    Can you explain how? Most of these look like essentially type-inference through duck-typing, and (AIUI) C++ doesn't even have duck-typing.
    - chombier 7y ago
      C++ templates are a kind of duck typing, aren't they?
    - jcelerier 7y ago
      C++ has had duck typing since it had generics. Here would be an example of the first case : https://wandbox.org/permlink/AIgZtkFgTuiQReDT https://wandbox.org/permlink/AIgZtkFgTuiQReDT
  - thesz 7y ago
    I agree, and some of these possible things can be more efficiently implemented in C++.
- skywhopper 7y ago
  Can you provide examples to show how Haskell and HList would solve the problems the author proposes?
maxfurman 7y ago
I'm not an expert on type systems, and maybe I'm misreading this gist, but doesn't Typescript work this way?
- _Codemonkeyism 7y ago
  As a TS user I'd think there is a lot of TS in this post, e.g. structural typing, union types etc.
- phiresky 7y ago
  Yep. The only thing missing is nominal aliases to primitive types, which is requested my many people [1] and even the TS compiler itself uses hacks to work around the lack of them. No idea why they don't add them already. Also of course any form of runtime type checking is missing. [1] https://github.com/Microsoft/Typescript/issues/202 https://github.com/Microsoft/Typescript/issues/202
- hateful 7y ago
  If this wasn't here I was going to put it. When using Vuejs with TypeScript, I consistently create interfaces for just the part of the data being returned from an API that I care about.
tobyhinloopen 7y ago
What I want from a gist document: Markdown, so I don’t have to scroll horizontally
- kirubakaran 7y ago
  You can just click the 'Raw' button/link for plain text: https://gist.githubusercontent.com/halgari/f431b2d1094e4ec1e933969969489854/raw/823f9ad204729aa00e02cacef20746b690f31357/gistfile1.txt https://gist.githubusercontent.com/halgari/f431b2d1094e4ec1e...
ufo 7y ago
There are some important requirements if you want to have "full type inference" in your language. In order: 1 - For each term in the language, there must be an unique "best type" that describes it. (principal type property) 2 - If principal types exist, then you also need to show that a type inference algorithm exists. (decidability of types) 3 - If the type inference algorithm exists, it must execute in a reasonable amount of time Many of the type system features that one might want to add to a language can violate one of these properties, specially when you start combining them together into a single type system. In particular, subtyping is particularly tricky. Finally, there is also a problem that you can never get away from with full global type inference schemes: type error messages tend to take the form of "type A is not equal to B" instead of "found type A, expected type B". Then a type constraint cannot be met, the error message cannot tell you which of the two sides is the wrong one. Additionally, the way that type constraints propagate means that the error message might not necessarily point to the true source of the type error. For these reasons, even in language with full type inference it is usually a good idea to at least have type annotations for top level functions.
sdegutis 7y ago
It's really interesting to see so many people going back and forth between dynamically typed languages Clojure and Elixir, and statically typed languages like OCaml and Haskell. Lately I've even started to even question whether TypeScript is really worth the trouble and slowness it's causing. I wrote about it briefly here: https://sdegutis.com/2019-06-20-considering-removing-typescript https://sdegutis.com/2019-06-20-considering-removing-typescr... On one hand, TypeScript's type system is extremely convenient when mixed with VS Code. On the other hand, it's getting slower and slower, which is making it actually counterproductive. I often wonder if I'd be faster in just plain JS.
- jzoch 7y ago
  What you've found might be that because you had this explicit contract (types) that coerced you to write your code in a certain way, your code looks simpler when you just turn the types off. But would you have written it this way had there been no types? This exercise is more similar to converting a typed language like java to a type inferenced one (a la java 12 or "auto" in C++11). If you didnt have the guard rails of types the way you built your system may differ by relying a lot more on runtime behavior and conventions rather than compile time type checking and explicitly enforced rules.
  - sdegutis 7y ago
    That's exactly what I aim to find out. But I don't feel very comfortable trying it on a client project, not yet at least. Having written in many statically and dynamically typed languages, I feel like I should have already come to a conclusion by now. Yet somehow I'm still on the fence after all these years.
deleted 7y ago
[deleted]
mcguire 7y ago
No parametric polymorphism?
gambler 7y ago
I've recently listened to a podcast (2004) with the author of Newspeak. Mind-expanding stuff that makes a lot of sense in retrospect. https://www.se-radio.net/2009/07/episode-140-newspeak-and-pluggable-types-with-gilad-bracha/ https://www.se-radio.net/2009/07/episode-140-newspeak-and-pl...
tathougies 7y ago
Number 3 is completely not what you want. I mean, you want that in certain cases, but you may also want the exhaustiveness checking. There needs to be two distinct notions here. The notion of a type should convey totality -- this value has a particular 'shape'. The notion described here is not a type, but more like an interface or a trait. In either case, it falls under polymorphism. Person as described here is not a type. That being said, all these things are implemented in PureScript, I believe.
deleted 7y ago
[deleted]
NikkiA 7y ago
Given his use of s-expressions, Carp-lang is probably exactly what he wants, but will probably be disappointed when he discovers just how much hoop-jumping there is to deal with non-GC type lifetime management. (unless he finds splattering `ref` and `copy` (or their syntactic sugar of `&` and `@`) in his code acceptable, in which case, congrats!)
deleted 7y ago
[deleted]
mamcx 7y ago
This is not solved by the relational model? I have think about this for my toy relational lang, I consider too the best is allow: fun print(people:People[id, name])... to work with any relation/class/struct that at least have that 2 fields. Also, in the relational model the name of the relation and the header is significant. Plus, re-combining of types is inbuilt. Need to extent person? rel Customer Person join Address, Phones...
_halgari 7y ago
Author here, a few things to keep in mind: Firstly, I wrote this about 3.5 years ago. I was wondering why people were suddenly commenting on it and now it all makes sense. Part of the fun of writing articles about this is watching everyone argue about what language can be forced into representing types in a given way. Yes, I assume in any situation that if I want a feature X in a type system, that somehow Haskell can be forced to give me that feature, but that doesn't necessarily mean it will fit with the ecosystem of the language or that that's the only feature I'm looking for in the language. So saying "someone hasn't done their homework if they think X can't be done" isn't relevant, what is relevant that I'm not aware of a language that provides the type system features I want combined with acceptable set of trade-offs. So anyways, I'll stick around for awhile and see if I can answer any questions. Thanks for the discussion, all!
- contravariant 7y ago
  I'm somewhat curious why you'd want both (2) and (3) to hold. Isn't it somewhat contradictory to want types to not just merely denote the structure, while requiring that everything with the same structure satisfies the type? Maybe it's because I'm influenced by C# but viewed from that perspective it would be like requiring you to explicitly declare that e.g. some value is a ProductID but when you're declaring a type you wouldn't need to declare it is a Person, provided it simply implements the right fields (in C# you would have to explicitly implementing some interface to clarify that first-name and last-name do indeed refer to a person and not, for example, the head and tail of a list of names). This does mean that any external code can't implement your interfaces though, which is a bit annoying, though fixable.
  - jdmichal 7y ago
    That's commonly called "duck-typing". And since you're discussing C#, I'll throw in that Typescript (another MS language) has duck-typing for interfaces. You can explicitly implement an interface, in which case the compiler will enforce that the interface is implemented. But you can also implicitly meet an interface.
stcredzero 7y ago
2) Value types in structures would need to be nominal, not structural. I really don't care if I get a tuple of [Int32, String], I very rarely care what the machine level types are, what I really want is [ProductID, ProductName], what the underlying types are doesn't really matter to me. In Go, there's a practice called "microtyping" (credit goes to HN user jerf) where everything is type defined to a semantic name. So you never have a struct with a string for ProductID and ProductName. Instead, you have a struct containing a ProductID and a ProductName. This makes it very easy to change your mind. I used to have a base64 encoded UUID as an EntityID in my MMO. I implemented microtyping, and after that, changing EntityID to 128 bits was a breeze!
- dvlsg 7y ago
  F# is good for this, too. It _kind_ of works in typescript, but it's not enforced by tsc. Definitely helps readability, though.
ben509 7y ago
I'm working on one [1] and doing the inference now, which is kicking my ass TBH, so some thoughts: > 1) Full type inference. Really, while writing and hacking, you want it, but ideally the system should be able to fill in your types for you. Note, though, that there's a tradeoff: the more overloading and other conveniences, the less complete the inference can be. In the system I'm working on, it's intended to deploy a library + documentation, so all types would be annotated in the artifact generated regardless of whether they are in the source. > 2). Value types in structures would need to be nominal, not structural. My answer to this is we want cheap sum types. In Tenet, a sum type can be constructed without any declaration by writing tag~expr. This implicitly defines Union[tag~WhateverExprTypeIs]. Since unions implicitly combine, if I have one branch return meters~55 another can return error~"something broke" and the return type overall is implicitly Union[meters~Integer, error~String]. The idea of declaring that, e.g. meters~X and centimeters~Y are interchangeable representations of the same value is something I'm thinking about; it's getting at a facility for encapsulation. > 3) Collections of [product types] would need to be inclusively typed, not exclusive. So, if we have syntax for retrieving an attribute `x.a + x.b` and we know + takes integers, we can deduce an assertion that x is some product type with two integer attributes a and b. I call that an open tuple, as opposed to a closed tuple. But all product types must be closed (exclusive) in order to construct them, obviously, and for non-dynamic languages, it seems like you're liable to have code size explosion (multiple copies of functions to support each type used) if you allow polymorphism this way. > 4) ... it would be important to have all these structural members be namespaced as well. I'm curious what people think the best namespace schemes are, because most of them seem like a lot of complexity for what they do. But... > 5) Now I would still need basic set logic for these types It won't make the first cut, but the basic operations would be sum and diff (for sum types), times and project (for product types) and a renaming facility with globbing seems like it might answer #4 just fine. [1]: https://tenet-lang.org/types.html#tenets-approach https://tenet-lang.org/types.html#tenets-approach
- CuriousSkeptic 7y ago
  I found it interesting that you tag the types like that. I’m working on a small language idea right now where I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name (borrowing the rdf model here) So (n1: v1) might be a value v1 bound to n1. And (n2: v2) another. (n1: v1)(n2: v2) = (n1: v1, n2: v2), and one could even imagine (n1: v1, n2: v2)(n3: n1+n2) as a valid expression. Which of course is equivalent to ( n1: v1, n2: v2, n3: n1+n2, ) not entirely unlike a let-expression (I’m thinking of unifying terms and types so a lambda would simply be such an expression where v1 and v2 are types) Oh well just a toy in my head at the moment. Just found it interesting to see similar tag combining semantics. (As for namespace I was thinking to borrow the plan9 approach of binding things dynamically, using something like Scalas implicits, for evaluation to do a kind of dependency injection thing, but a global lexically scoped tree for typing it)
mywittyname 7y ago
I want from a type system the ability to quickly understand the data structures involved in this code that I'm debugging which was written several years ago by developers who've long since moved on. The more clever, independent, and unbound you are, the less you appreciate types, because you never really feel the pain points that types alleviate.
deleted 7y ago
[deleted]

106 points by grzm 7y ago

Honestly you can nearly write Haskell without specifying type signatures. GHC is very sophisticated. I feel like there have only been a few situations where I actually needed to specify the type. Really the argument shouldn't be about having strict types vs dynamic, it should be about smarter compilers etc. To me, GHC seems to be nearly perfect (also GHCi).

87zuhjkas 7y ago
I agree, GHC has the best type inference that I know of.
nestorD 7y ago
Ocaml also standout as a language in which you can omit type definitions (the only exception I ever needed was when deserializing data).
- aloisdg 7y ago
  In the same vein F# as a descendant of OCaml, opens all of this fot the .Net world.
  - nestorD 7y ago
    F# adds a [] operator to access containers (mostly arrays and dictionnaries) and unifies arithmetic operators (no more +.). While I believe those make for a more streamlined language (I do prefer F# to Ocaml), it also means that you regularly need type signature to desambiguate things where nothing was needed in Ocaml.
deleted 7y ago
[deleted]
yogthos 7y ago
HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct. Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to understand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety. Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort. [1] https://github.com/davidfstr/idris-insertion-sort/blob/master/InsertionSort.idr https://github.com/davidfstr/idris-insertion-sort/blob/maste...
- Drup 7y ago
  This is really an apple to oranges comparison. What you linked is not an implementation of the insertion sort. It's a an implementation coupled with proof of correctness. Try to make a mechanize proof of correctness of your python code, and it'll be as long (or longer). If you just write an implementation in statically typed languages like OCaml, F#, Haskell, Typescript (or even Idris, if you go less crazy with the typing), and you can get it down to less 10 lines easily.
  - yogthos 7y ago
    A proof of correctness is what static typing is fundamentally. The example I provided simply turns this up to 11. However, if you relax the constraint then you're losing benefits of statically checking properties at compile time. If you agree that having a 10 line version that does less checking is better than having a 260 line version that does, then you're agreeing that there is a cost associated with static checking. There are plenty of real world scenarios where static checking gets in the way even if you're not trying to encode complex properties using the type system. One problem is that static typing is at odds with modularization since type declarations are considered globally. For example, Ring HTTP abstraction in Clojure represents requests and responses as maps. Middleware functions [1] can update these maps to inject additional keys, or modify existing keys. These functions often live in separate libraries that know nothing about one another. A static type system precludes this since it would require you to provide a static declaration for every possible request and response map. [1] https://github.com/ring-clojure/ring/wiki/Middleware-Patterns https://github.com/ring-clojure/ring/wiki/Middleware-Pattern...

cjfd 7y ago

I don't agree with this at all. Having the types of every variable written explicitly in the code is important documentation that answers very quickly the question 'what is the type of this thing' without having to look everywhere and anywhere to perhaps find out that it could be any one of three types. If you do not know the type of something you also do not know what operations are available on that thing.

empath75 7y ago
Use an IDE
- wereHamster 7y ago
  I'm not always using an IDE when looking at code. Sometimes I read code directly on GitHub, or repl.it, or codesandbox, or ….
  - Waterluvian 7y ago
    Maybe those can evolve further too. I've always appreciated the advantages of code being legible as plain text files. But maybe it is just a little absurd when language design is shaped to fit the desire not to evolve the storage format and editing interface.
  - azhenley 7y ago
    I agree with your comment. GitHub does seem to be moving towards adding IDE-like features though: https://github.com/github/semantic https://github.com/github/semantic
pjc50 7y ago
It looks like there's two very different styles going on here. Most of us are used to the OO-type approach (Java, C#) where the operations are "inside" the object and defined on it. This article is coming from a very different place where the operations are "outside" the typed things, which are more like structs, and the programmer can write any operation that takes structs which have the right fields. The author doesn't make any comment on dispatch let alone multiple dispatch. They appear to be writing for the kind of quasi-schema'd information bureaucracy that's very important outside of SV. Lots of data in XML that never quite lines up with an object model. The Haskellite approach would also say that "what operations are available on that thing" is the wrong way round; you define your operation, and the type signature tells you what kind of things will work with it.

yakshaving_jgt 7y ago

…Sounds like he just wants row polymorphism, no?

karmakaze 7y ago

> Value types in structures would need to be nominal The reasoning behind wanting this is good. It can however be satisfied differently. I find structural typing to be more convenient where I have the ability to define a type for another that is not considered to be equivalent. A good example is how an int can be defined into different types with conversions in Go. If we were to follow through with nominal typing we would need transforms to rename the same structures when working through abstractions that make sense having different names.

thesz 7y ago

This is the case when someone didn't completed his homework. Most of things he requested are possible with HList in Haskell. A library, nonetheless. From 2008, I believe. PS Structural subtyping is tricky: https://pdfs.semanticscholar.org/ff6f/1c49ff00efa483807fae71ef2a0f2baf6a04.pdf https://pdfs.semanticscholar.org/ff6f/1c49ff00efa483807fae71... It took quarter of century to get it right. Most probably the author of gist just don't get it's trickyness yet.

gpderetta 7y ago
in fact, most of those things are possible in c++ of all places.
- ken 7y ago
  Can you explain how? Most of these look like essentially type-inference through duck-typing, and (AIUI) C++ doesn't even have duck-typing.
  - chombier 7y ago
    C++ templates are a kind of duck typing, aren't they?
  - jcelerier 7y ago
    C++ has had duck typing since it had generics. Here would be an example of the first case : https://wandbox.org/permlink/AIgZtkFgTuiQReDT https://wandbox.org/permlink/AIgZtkFgTuiQReDT
- thesz 7y ago
  I agree, and some of these possible things can be more efficiently implemented in C++.
skywhopper 7y ago
Can you provide examples to show how Haskell and HList would solve the problems the author proposes?

maxfurman 7y ago

I'm not an expert on type systems, and maybe I'm misreading this gist, but doesn't Typescript work this way?

_Codemonkeyism 7y ago
As a TS user I'd think there is a lot of TS in this post, e.g. structural typing, union types etc.
phiresky 7y ago
Yep. The only thing missing is nominal aliases to primitive types, which is requested my many people [1] and even the TS compiler itself uses hacks to work around the lack of them. No idea why they don't add them already. Also of course any form of runtime type checking is missing. [1] https://github.com/Microsoft/Typescript/issues/202 https://github.com/Microsoft/Typescript/issues/202
hateful 7y ago
If this wasn't here I was going to put it. When using Vuejs with TypeScript, I consistently create interfaces for just the part of the data being returned from an API that I care about.

tobyhinloopen 7y ago

What I want from a gist document: Markdown, so I don’t have to scroll horizontally

kirubakaran 7y ago
You can just click the 'Raw' button/link for plain text: https://gist.githubusercontent.com/halgari/f431b2d1094e4ec1e933969969489854/raw/823f9ad204729aa00e02cacef20746b690f31357/gistfile1.txt https://gist.githubusercontent.com/halgari/f431b2d1094e4ec1e...

ufo 7y ago

There are some important requirements if you want to have "full type inference" in your language. In order: 1 - For each term in the language, there must be an unique "best type" that describes it. (principal type property) 2 - If principal types exist, then you also need to show that a type inference algorithm exists. (decidability of types) 3 - If the type inference algorithm exists, it must execute in a reasonable amount of time Many of the type system features that one might want to add to a language can violate one of these properties, specially when you start combining them together into a single type system. In particular, subtyping is particularly tricky. Finally, there is also a problem that you can never get away from with full global type inference schemes: type error messages tend to take the form of "type A is not equal to B" instead of "found type A, expected type B". Then a type constraint cannot be met, the error message cannot tell you which of the two sides is the wrong one. Additionally, the way that type constraints propagate means that the error message might not necessarily point to the true source of the type error. For these reasons, even in language with full type inference it is usually a good idea to at least have type annotations for top level functions.

sdegutis 7y ago

It's really interesting to see so many people going back and forth between dynamically typed languages Clojure and Elixir, and statically typed languages like OCaml and Haskell. Lately I've even started to even question whether TypeScript is really worth the trouble and slowness it's causing. I wrote about it briefly here: https://sdegutis.com/2019-06-20-considering-removing-typescript https://sdegutis.com/2019-06-20-considering-removing-typescr... On one hand, TypeScript's type system is extremely convenient when mixed with VS Code. On the other hand, it's getting slower and slower, which is making it actually counterproductive. I often wonder if I'd be faster in just plain JS.

jzoch 7y ago
What you've found might be that because you had this explicit contract (types) that coerced you to write your code in a certain way, your code looks simpler when you just turn the types off. But would you have written it this way had there been no types? This exercise is more similar to converting a typed language like java to a type inferenced one (a la java 12 or "auto" in C++11). If you didnt have the guard rails of types the way you built your system may differ by relying a lot more on runtime behavior and conventions rather than compile time type checking and explicitly enforced rules.
- sdegutis 7y ago
  That's exactly what I aim to find out. But I don't feel very comfortable trying it on a client project, not yet at least. Having written in many statically and dynamically typed languages, I feel like I should have already come to a conclusion by now. Yet somehow I'm still on the fence after all these years.

deleted 7y ago

[deleted]

mcguire 7y ago

No parametric polymorphism?

gambler 7y ago

I've recently listened to a podcast (2004) with the author of Newspeak. Mind-expanding stuff that makes a lot of sense in retrospect. https://www.se-radio.net/2009/07/episode-140-newspeak-and-pluggable-types-with-gilad-bracha/ https://www.se-radio.net/2009/07/episode-140-newspeak-and-pl...

tathougies 7y ago

Number 3 is completely not what you want. I mean, you want that in certain cases, but you may also want the exhaustiveness checking. There needs to be two distinct notions here. The notion of a type should convey totality -- this value has a particular 'shape'. The notion described here is not a type, but more like an interface or a trait. In either case, it falls under polymorphism. Person as described here is not a type. That being said, all these things are implemented in PureScript, I believe.

deleted 7y ago

[deleted]

NikkiA 7y ago

Given his use of s-expressions, Carp-lang is probably exactly what he wants, but will probably be disappointed when he discovers just how much hoop-jumping there is to deal with non-GC type lifetime management. (unless he finds splattering `ref` and `copy` (or their syntactic sugar of `&` and `@`) in his code acceptable, in which case, congrats!)

deleted 7y ago

[deleted]

mamcx 7y ago

This is not solved by the relational model? I have think about this for my toy relational lang, I consider too the best is allow: fun print(people:People[id, name])... to work with any relation/class/struct that at least have that 2 fields. Also, in the relational model the name of the relation and the header is significant. Plus, re-combining of types is inbuilt. Need to extent person? rel Customer Person join Address, Phones...

_halgari 7y ago

Author here, a few things to keep in mind: Firstly, I wrote this about 3.5 years ago. I was wondering why people were suddenly commenting on it and now it all makes sense. Part of the fun of writing articles about this is watching everyone argue about what language can be forced into representing types in a given way. Yes, I assume in any situation that if I want a feature X in a type system, that somehow Haskell can be forced to give me that feature, but that doesn't necessarily mean it will fit with the ecosystem of the language or that that's the only feature I'm looking for in the language. So saying "someone hasn't done their homework if they think X can't be done" isn't relevant, what is relevant that I'm not aware of a language that provides the type system features I want combined with acceptable set of trade-offs. So anyways, I'll stick around for awhile and see if I can answer any questions. Thanks for the discussion, all!

contravariant 7y ago
I'm somewhat curious why you'd want both (2) and (3) to hold. Isn't it somewhat contradictory to want types to not just merely denote the structure, while requiring that everything with the same structure satisfies the type? Maybe it's because I'm influenced by C# but viewed from that perspective it would be like requiring you to explicitly declare that e.g. some value is a ProductID but when you're declaring a type you wouldn't need to declare it is a Person, provided it simply implements the right fields (in C# you would have to explicitly implementing some interface to clarify that first-name and last-name do indeed refer to a person and not, for example, the head and tail of a list of names). This does mean that any external code can't implement your interfaces though, which is a bit annoying, though fixable.
- jdmichal 7y ago
  That's commonly called "duck-typing". And since you're discussing C#, I'll throw in that Typescript (another MS language) has duck-typing for interfaces. You can explicitly implement an interface, in which case the compiler will enforce that the interface is implemented. But you can also implicitly meet an interface.

stcredzero 7y ago

2) Value types in structures would need to be nominal, not structural. I really don't care if I get a tuple of [Int32, String], I very rarely care what the machine level types are, what I really want is [ProductID, ProductName], what the underlying types are doesn't really matter to me. In Go, there's a practice called "microtyping" (credit goes to HN user jerf) where everything is type defined to a semantic name. So you never have a struct with a string for ProductID and ProductName. Instead, you have a struct containing a ProductID and a ProductName. This makes it very easy to change your mind. I used to have a base64 encoded UUID as an EntityID in my MMO. I implemented microtyping, and after that, changing EntityID to 128 bits was a breeze!

dvlsg 7y ago
F# is good for this, too. It _kind_ of works in typescript, but it's not enforced by tsc. Definitely helps readability, though.

ben509 7y ago

I'm working on one [1] and doing the inference now, which is kicking my ass TBH, so some thoughts: > 1) Full type inference. Really, while writing and hacking, you want it, but ideally the system should be able to fill in your types for you. Note, though, that there's a tradeoff: the more overloading and other conveniences, the less complete the inference can be. In the system I'm working on, it's intended to deploy a library + documentation, so all types would be annotated in the artifact generated regardless of whether they are in the source. > 2). Value types in structures would need to be nominal, not structural. My answer to this is we want cheap sum types. In Tenet, a sum type can be constructed without any declaration by writing tag~expr. This implicitly defines Union[tag~WhateverExprTypeIs]. Since unions implicitly combine, if I have one branch return meters~55 another can return error~"something broke" and the return type overall is implicitly Union[meters~Integer, error~String]. The idea of declaring that, e.g. meters~X and centimeters~Y are interchangeable representations of the same value is something I'm thinking about; it's getting at a facility for encapsulation. > 3) Collections of [product types] would need to be inclusively typed, not exclusive. So, if we have syntax for retrieving an attribute `x.a + x.b` and we know + takes integers, we can deduce an assertion that x is some product type with two integer attributes a and b. I call that an open tuple, as opposed to a closed tuple. But all product types must be closed (exclusive) in order to construct them, obviously, and for non-dynamic languages, it seems like you're liable to have code size explosion (multiple copies of functions to support each type used) if you allow polymorphism this way. > 4) ... it would be important to have all these structural members be namespaced as well. I'm curious what people think the best namespace schemes are, because most of them seem like a lot of complexity for what they do. But... > 5) Now I would still need basic set logic for these types It won't make the first cut, but the basic operations would be sum and diff (for sum types), times and project (for product types) and a renaming facility with globbing seems like it might answer #4 just fine. [1]: https://tenet-lang.org/types.html#tenets-approach https://tenet-lang.org/types.html#tenets-approach

CuriousSkeptic 7y ago
I found it interesting that you tag the types like that. I’m working on a small language idea right now where I wanted to treat bindings as first class, and having them combine with row polymorphism into a construct subsuming tuples, argument lists, and environments into a kind of unified thing, with a similar result in mind. Even to the point of perhaps demoting scalars from first class status actually, point being that where there is a value there should be a name (borrowing the rdf model here) So (n1: v1) might be a value v1 bound to n1. And (n2: v2) another. (n1: v1)(n2: v2) = (n1: v1, n2: v2), and one could even imagine (n1: v1, n2: v2)(n3: n1+n2) as a valid expression. Which of course is equivalent to ( n1: v1, n2: v2, n3: n1+n2, ) not entirely unlike a let-expression (I’m thinking of unifying terms and types so a lambda would simply be such an expression where v1 and v2 are types) Oh well just a toy in my head at the moment. Just found it interesting to see similar tag combining semantics. (As for namespace I was thinking to borrow the plan9 approach of binding things dynamically, using something like Scalas implicits, for evaluation to do a kind of dependency injection thing, but a global lexically scoped tree for typing it)

mywittyname 7y ago

I want from a type system the ability to quickly understand the data structures involved in this code that I'm debugging which was written several years ago by developers who've long since moved on. The more clever, independent, and unbound you are, the less you appreciate types, because you never really feel the pain points that types alleviate.

deleted 7y ago

[deleted]