Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Dynamic type systems are not inherently more open

lexi-lambda.github.io

Post reply on HN
Print view View original

241–250 of 286 posts

Re: Dynamic type systems are not inherently more open

#241

Post by yawaramin »

azhenley wrote: post #237
sweeneyrod wrote: post #233

Earlier quoted context omitted.

If type inference damaged readability, we would expect companies/projects that use languages such as OCaml and Haskell where type inference is possible but not mandatory to have policies against it in their style guides. In my experience with OCaml, the widely agreed on style is to only annotate types of functions that are part of some public interface (although since this annotation is necessary to define the public…

Companies do have policies against using type inference (e.g., the use of var in C#). But how would companies/people know if it damaged readability? There has been little research on this (a few studies are currently in peer review!) and our intuition about such things is often inaccurate. There are so many other confounding factors that it is hard to isolate just type inference/annotations.

> Companies do have policies against using type inference (e.g., the use of var in C#).

That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?

Re: Dynamic type systems are not inherently more open

#242

Post by chrisdone »

pron wrote: post #95
UglyToad wrote: post #29

I think there's a perhaps irreconcilable disconnect between 2 camps here, but I also think that's ok and different people are allowed to like different things. My experience, having gone from dynamic typing to static typing and now pining for more expressive type features in my chosen language is that static typing changes where you have to spend the cognitive complexity budget. To my mind if I return to a piece of d…

Not all untyped languages are the same. E.g. Clojure now encourages specifying assumptions with spec annotations, some of them are stronger than those that can be expressed by Haskell's type system: i.e. they can succinctly express more about the "entire code" than Haskell's types. Types are not the only way to write formal assertions and assumptions about code. The difference between the two is in the level of sound…

Techniques like Ghost of Departed Proofs are the most exciting thing to me as a casual correctness enthusiast. It acts as a means of combining static types with contracts.

Types are sound mostly because they are a stupid mini language, so easily enforced, like you said. Contracts are practical and convenient because you tend to write them in the language or a subset thereof that you’re checking. That’s hard to ignore.

GODP has you write a runtime check in regular code, and return as a result a proof value. Put that code in a module boundary. Then you have upstream functions expect a proof argument along with the value the proof is about. They’re tied together with a unique type variable (rank n or existential are the mechanisms of delivery for Haskell, but may differ in other languages).

head :: NonEmpty n -> Named n (List a) -> a

In this way you started from a dynamic, runtime piece of code, and ended up using a static type system to just ensure everything is passed around correctly which is trivial.

A single proof in this technique is nominal in the type (e.g. not null or positive or sorted ascending/descending), but combining them is done at the value level so there’s flexibility.

The bang for buck potential is large. I’m more interested in stuff like this than the dependent types direction that people are pushing for in GHC. If I wanted dependent types I have Agda, Coq, Isabelle, Idris, etc. to play with.

Re: Dynamic type systems are not inherently more open

#243

Post by [deleted] »

azhenley wrote: post #237
sweeneyrod wrote: post #233

Earlier quoted context omitted.

If type inference damaged readability, we would expect companies/projects that use languages such as OCaml and Haskell where type inference is possible but not mandatory to have policies against it in their style guides. In my experience with OCaml, the widely agreed on style is to only annotate types of functions that are part of some public interface (although since this annotation is necessary to define the public…

Companies do have policies against using type inference (e.g., the use of var in C#). But how would companies/people know if it damaged readability? There has been little research on this (a few studies are currently in peer review!) and our intuition about such things is often inaccurate. There are so many other confounding factors that it is hard to isolate just type inference/annotations.

[deleted]

Re: Dynamic type systems are not inherently more open

#244

Post by azhenley »

yawaramin wrote: post #241
azhenley wrote: post #237

Earlier quoted context omitted.

Companies do have policies against using type inference (e.g., the use of var in C#). But how would companies/people know if it damaged readability? There has been little research on this (a few studies are currently in peer review!) and our intuition about such things is often inaccurate. There are so many other confounding factors that it is hard to isolate just type inference/annotations.

> Companies do have policies against using type inference (e.g., the use of var in C#). That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?

Yes! Any company that has adopted MyPy or TypeScript often have policies for this. One team I spoke to at Facebook said that any new code should have type annotations. I believe Dropbox had a nice blog post about new code should have type annotations too. It is hard to get these details from companies/teams (and be allowed to talk about it).

Re: Dynamic type systems are not inherently more open

#245

Post by sweeneyrod »

azhenley wrote: post #244
yawaramin wrote: post #241

Earlier quoted context omitted.

> Companies do have policies against using type inference (e.g., the use of var in C#). That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?

Yes! Any company that has adopted MyPy or TypeScript often have policies for this. One team I spoke to at Facebook said that any new code should have type annotations. I believe Dropbox had a nice blog post about new code should have type annotations too. It is hard to get these details from companies/teams (and be allowed to talk about it).

Do they mandate that only function types (and any ambiguous ones) should be annotated, or that all types (i.e. including those of local variables which mypy can infer) should be? I strongly suspect the former, which implies that they view type annotations more as a necessary evil to allow type checking rather than a benefit in their own right. After all, there was nothing stopping people putting "type annotations" in Python 2.5 code if you wanted, by writing `x = get_thing_count() # int`. But AFAIK no-one did that until annotations could actually be used to check type safety.

Re: Dynamic type systems are not inherently more open

#246

Post by caseymarquis »

galangalalgol wrote: post #234
caseymarquis wrote: post #210

Earlier quoted context omitted.

YMMV. There's probably at least one good use case for virtually every design. What you're doing could be totally reasonable. The original description sounded like 13 functions being manually chained together, each inside the last. Where to go from there is very situational. Using a POC is pretty much a given. For transformation in the simplest form, I'd typically have a series of extension methods (or some equivalent…

I'm keeping that line. More wrong places... That is koan worthy. What is DI dynamic initialization? I can't imagine passing a const bit of POD through 13 layers without it bein used, but not every layer uses all of it probably.

Dependency injection.

It's basically a fancy way of saying 'Use reflection to read all of the dependencies that exist in my code, and then automatically initialize those dependencies and pass them to the classes which need them.' This (for me) is a recursive process which starts at root "singleton" objects (single per DI session), then moves down through the tree that is my code and its dependencies.

Typically, dependencies are passed via constructor then stored in a field. I personally think that's a dumb way to do it, as I'm using DI to eliminate boilerplate code, and you don't often get code more boilerplate and tedious than copying a variable into a field. I instead mark fields with obvious attributes that show that DI is used for initialization, then have my DI framework automatically fill them in.

People often overuse interfaces with DI, which leads to very difficult to trace code. I consider that an anti-pattern unless writing a library for others. Unfortunately, I think the people doing this have made DI seem like a trade off: you remove boilerplate code, but you lose clarity. You'll see this in virtually every DI tutorial, which is unfortunate. DI can be done just as well with concrete objects.

If you're using a language with reflection, I'd highly recommend learning a DI framework. Once you've figured out what you don't like you can find a framework that works the way you prefer, or in the worst case write your own. You definitely have to structure your code for DI, and it's difficult to add after the fact. That said, I was able to chop 5 to 10k lines off a 100k project I converted last year, and more importantly adding new functionality became much faster and easier. Again YMMV.

Re: Dynamic type systems are not inherently more open

#247

Post by yawaramin »

azhenley wrote: post #244
yawaramin wrote: post #241

Earlier quoted context omitted.

> Companies do have policies against using type inference (e.g., the use of var in C#). That's a language that historically has not had type inference. Any examples of companies mandating type annotations in historically type-inferred languages?

Yes! Any company that has adopted MyPy or TypeScript often have policies for this. One team I spoke to at Facebook said that any new code should have type annotations. I believe Dropbox had a nice blog post about new code should have type annotations too. It is hard to get these details from companies/teams (and be allowed to talk about it).

That's because (a) these are not historically type-inferred languages–runtime typechecking doesn't count as type inference–and (b) the gradual typechecking approaches like Mypy and TypeScript often have a lot of type inference issues which force people to try to overcome them with manual annotations.

In languages with even reasonably good type inference you'll find that the idiom is not to annotate types at the very least inside function bodies. And in OCaml, which has principality of type inference i.e. the types it infers cannot be overridden and corrected by manual annotation, the idiom is to not annotate implementation files at all.

Re: Dynamic type systems are not inherently more open

#248

Post by candeira »

roenxi wrote: post #228
yakshaving_jgt wrote: post #110

Earlier quoted context omitted.

> Clojure for example, goes beyond types with it's abstractions (like seq, that can be applied to strings, lists, maps and so on) Goes beyond types? Statically-typed languages can have polymorphism.

Spec is at heart a data modelling system. So for example, (s/def ::integer integer?) is very explicitly not a definition of an "integer" type. It is preparation to model some data x and check that the data will evaluate to true if someone uses the predicate (integer? x). However, this is obviously enough to implement a type system. But you can also do some very loose things with spec that aren't done in a type system…

> But you can also do some very loose things with spec that aren't done in a type system (I speak with a cheerful ignorance of type systems). Eg, I can spec a function so that one argument is smaller than the second. This allows my testing system to automatically generate the correct data to test my function.

Check out dependent type systems. These allow you to define, mindbreakingly enough, types that __depend on the values you assign at runtime__, and functions whose type depends on the values passed as arguments.

Don't ask me how it's done; it's all dark magic to me. All I know is that people who use dependent type systems claim they are very good at certain uses involving incoming streams of unknown data, like parsing binary protocols.

https://en.wikipedia.org/wiki/Dependent_type

Re: Dynamic type systems are not inherently more open

#249

Post by NicoJuicy »

beders wrote: post #134
NicoJuicy wrote: post #40

Earlier quoted context omitted.

I actually rely on static typing to make architectural code changes. Why I would want to go to dynamic typing is beyond me. My performance/efficiency would greatly decrease. . The next change I will implement will likely be to not allow null in a property, which can be done in c# 8

The idea is that you wouldn't need large refactorings in more dynamic languages in the first place since you are operating on a different abstraction level.

Lol, most of refactoring is bad code or not future-proof code.

Dynamic typing won't help with that.

Re: Dynamic type systems are not inherently more open

#250

Post by Izkata »

erik_seaberg wrote: post #222
sethev wrote: post #189

Earlier quoted context omitted.

I thought the article was good and addressed a real point of confusion, as evidenced by the two included comments (from Reddit and HN). You can consume arbitrary data using a program written in a statically typed or dynamically typed language. Whether it's decoupled from changes in the data depends on how the code is written and the data model, which have nothing to do with static vs dynamic typing. To me the stronge…

> the boundary between programs is dynamically typed Many interfaces have declared, enforced static types. I don't have to write any code to handle SELECT birthdate FROM employees WHERE id = ? returning "fish" because the database would never let it happen.

So you say, but sqlite has no problem with you storing "fish" in an integer column.
Post reply on HN