Dynamic type systems are not inherently more open • Hacker News Board

Re: Dynamic type systems are not inherently more open

#251

Post by dwohnitmok » Mon, Jan 20, 2020, 3:32 AM UTC

chrisdone wrote: post #242

pron wrote: post #95

Earlier quoted context omitted.

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…

Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure).

Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to express associativity with a contract system. Contract systems are very well-suited for imperative contexts (see e.g. Hoare Logic), where you have procedures rather than functions and you usually don't think about e.g. whether a procedure is associative or not. They work for functions, but are not as great a fit.

Dependent types allow for further expressivity, and, crucially, as long as you separate theorems from code (that is as long as you don't take Curry-Howard too seriously), there's no reason you're forced to prove a theorem with the type system if you find it too difficult.

Imagine:

concat : List a -> List a -> List a

concat = ...

concatSumsLength : (xs : List a) -> (ys : List a) -> size (concat xs ys) = size xs + size ys

concatSumsLength = proofByPropertyTest concatPropertyTest

concatPropertyTest = (1000 different lists concatenated together and then checking that their sizes add up)

There's no reason that concatSumsLength needs to be satisfied by a true implementation, unless you require that its value be usable at runtime. However, as Idris 2 shows, there's no need for that to be true (or even Coq with Prop vs Type). You can just annotate it as erased at runtime.

If you have a way of ensuring that certain values are never used at runtime, then there is no reason that your proof obligations must be met through satisfying the type checker.

Re: Dynamic type systems are not inherently more open

#252

Post by kazinator » Mon, Jan 20, 2020, 5:32 AM UTC

sethev wrote: post #189

svat wrote: post #90

Six notable things I took away from this post: - Structural typing, i.e. instead of "you eagerly write a schema for the whole universe", just limit to what you need (basically, encode only the same kinds of assumptions you would make in a dynamically-typed language). - It’s easy to discover the assumptions of the Haskell program [...] In the dynamically-typed program, we’d have to audit every code path — Left implici…

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…

> You can consume arbitrary data using a program written in a statically typed or dynamically typed language.

Really? Okay, below is something that meets the definition of "arbitrary data". Can some static program process it and evoke its full meaning without the programmer having to develop an ad-hoc dynamic typing system?

  (defun defset-expander (env macform name params newval setform)
    (with-gensyms (getter setter args gpf-pairs gpr-pairs ext-pairs
                   pgens rgens egens all-pairs agens nvsym)
      (let* ((ap (analyze-params params))
             (exp-params (car ap))
             (total-syms (cadr ap))
             (fp (new fun-param-parser form macform syntax exp-params))
             (fixpars (append fp.req fp.(opt-syms)))
             (restpar (if (symbol-package fp.rest) fp.rest))
             (extsyms [keep-if symbol-package
                               (diff total-syms (cons restpar fixpars))])
             (xsetform ^^(alet ((,',nvsym ,,newval))
                           ,,(expand ^(symacrolet ((,newval ',nvsym))
                                        ,setform)
                                     env))))
        ^(defplace (,name . ,args) body
           (,getter ,setter
             (tree-bind ,params ,args
               (let* ((,gpf-pairs (mapcar (op (fun list) (gensym)) (list ,*fixpars)))
                      (,gpr-pairs (if ',restpar
                                    (if (consp ,restpar)
                                      (mapcar (op (fun list) (gensym)) ,restpar)
                                      (list (list (gensym) ,restpar)))))
                      (,ext-pairs (mapcar (op (fun list) (gensym)) (list ,*extsyms)))
                      (,pgens (mapcar (fun car) ,gpf-pairs))
                      (,rgens (mapcar (fun car) ,gpr-pairs))
                      (,egens (mapcar (fun car) ,ext-pairs))
                      (,all-pairs (append ,gpf-pairs ,gpr-pairs ,ext-pairs))
                      (,agens (collect-each ((a ,args))
                               (let ((p (pos a ,all-pairs (fun eq) (fun cadr))))
                                 (if p
                                   (car (del [,all-pairs p]))
                                   a)))))
                 ^(alet (,*,gpf-pairs ,*,gpr-pairs ,*,ext-pairs)
                    ,(expand ^(symacrolet (,*(zip ',fixpars
                                                  (mapcar (ret ^',@1) ,pgens))
                                           ,*(zip ',extsyms
                                                  (mapcar (ret ^',@1) ,egens))
                                           ,*(if ,gpr-pairs
                                               (if (consp ,restpar)
                                                 ^((,',restpar ',,rgens))
                                                 ^((,',restpar ',(car ,rgens))))))
                                (macrolet ((,,getter () ^(,',',name ,',*,agens))
                                           (,,setter (,',newval)
                                              ,',xsetform))
                                  ,body))
                             ,env)))))))))

Re: Dynamic type systems are not inherently more open

#253

Post by kazinator » Mon, Jan 20, 2020, 7:02 AM UTC

mokus wrote: post #206

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…

> If systems that extend beyond a single program require dynamic typing, doesn't it make sense to invest more in ways to do dynamic typing better? Isn’t dynamic typing more or less a default state of not knowing anything at compile time about the values your data will take? One could equally well ask “given that the boundaries of our systems are necessarily characterized by unpredictability, doesn’t it make sense to…

No! The "default state" for not knowing anything at compile time about the values your data will take is typelessness, exemplified by machine-oriented languages like BCPL and most assembly languages. In this state, the machine knows nothing about the types of your values at any time. Each operation that you apply to a value just assumes that it has the right type for that operation.

Programs in such languages must be statically type checked --- by the coder.

Sometimes (usually?) those languages define the effects of type punning, so type mismatches are not necessarily errors. The programmer must know which are intentional (to be analyzed for correctness from a type-punning perspective) and which are bugs. This could come from comments or naming conventions.

Dynamic typing is a huge increment over this situation; what is surprising is how early the original Lisp people figured it out, while also inventing useful abstractions like symbols and whatnot.

Re: Dynamic type systems are not inherently more open

#254

Post by yakshaving_jgt » Mon, Jan 20, 2020, 7:54 AM UTC

kazinator wrote: post #252

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…

> You can consume arbitrary data using a program written in a statically typed or dynamically typed language. Really? Okay, below is something that meets the definition of "arbitrary data". Can some static program process it and evoke its full meaning without the programmer having to develop an ad-hoc dynamic typing system? (defun defset-expander (env macform name params newval setform) (with-gensyms (getter setter a…

Yes. A program written in a statically-typed programming language can parse the lisp you have written above.

Re: Dynamic type systems are not inherently more open

#255

Post by twic » Mon, Jan 20, 2020, 8:00 AM UTC

erdeszt wrote: post #50

alerighi wrote: post #33

Recently I worked on a project where initially we though about writing it in Rust, because why not, it seemed initially a good idea. It turned out to be a completely wrong idea. The project was a simple web API, nothing fancy, GraphQL and a SQL database. After a lot of frustrations we decided it to rewrite everything in TypeScript and did that in a week. TypeScript gives you the benefit of statically typed languages…

Why did you decide to use a system programming language to build a web api? That's 100% the wrong tool for the job.

There has been a movement in the Rust community to position it as good for backend web development. This is why there's been so much work on async, excitement about Actix, etc. It's not hugely surprising that this has given outsiders the impression that Rust might be a good choice for backend web development.

The reasons for this movement escape me. We already have many good options for backend web development. None of Rust's unique strengths offer any advantages for it. Focus on web has diverted effort from areas where Rust could really make a difference, like embedded, drivers, and desktop.

The best i can come up with is that a lot of people have come into Rust from other languages where web development is a big deal (eg Ruby), and it's just impossible for them to imagine that a language could be good and successful without winning at web development.

Re: Dynamic type systems are not inherently more open

#256

Post by choeger » Mon, Jan 20, 2020, 9:58 AM UTC

millstone wrote: post #235

choeger wrote: post #221

Earlier quoted context omitted.

I can easily write you pickle in Haskell. In fact you can easily embed Python's single type in Haskell and thus do everything you can do in python. The difference to Java has nothing to do with reflection, really, but rather with a uniform object representation (in Java you know the shape of all values by default).

I don’t believe one can write pickle.load in Haskell. Please show me how! A Java pickle.load would need to lean heavily on its dynamic features including reflection. For example, looking up a class by name.

Have a look at this typeclass, for instance:

https://hackage.haskell.org/package/base-4.12.0.0/docs/Type-...

If that's to complicated, just create an ADT of all the python values and translate Pickle's implementation directly.

Re: Dynamic type systems are not inherently more open

#257

Post by chrisdone » Mon, Jan 20, 2020, 10:01 AM UTC

dwohnitmok wrote: post #251

chrisdone wrote: post #242

Earlier quoted context omitted.

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…

Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure). Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to…

That's an interesting angle. Another way of saying it might be that GoDP on the face of it can make one-off proofs for a value. Proofs for a function requires making proofs about all possible inputs, which is where your property test comes in handy. I could have `Named a (List x -> List x -> List x)` as the function I'm proving things about.

With some template-haskell you could run the property test at compile-time, and then use that proof later (e.g. for an instance of Semigroup which would require a argument proof of associativity), in languages like Unison that never run the same test suite twice (due to Content addressable code), this would be feasible. Or just run the property in your test suite and hope that the developer runs the test suite often. GHC erases data types that aren't actually evaluated in many contexts, so we even have erasure too.

I like your angle!

Re: Dynamic type systems are not inherently more open

#258

Post by pron » Mon, Jan 20, 2020, 11:20 AM UTC

dwohnitmok wrote: post #251

chrisdone wrote: post #242

Earlier quoted context omitted.

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…

Actually techniques like the Ghost of Departed Proofs are precisely the reason I'm excited about dependent types (although with the caveat that you need some way of talking about erasure). Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves. For example, it's rather convoluted to…

> Contract systems in general have the problem that it is difficult to express higher-order properties about how functions should interact with each other or repeated invocations of themselves

Contract systems can express anything that can be expressed about a program. Some allow you to specify separate lemmas (e.g. see http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/jmlrefman_toc...) . The difference between dependent types and contract systems is that contract systems can be verified by deductive proofs, or by a host of unsound techniques, while dependent types require deductive proof (or, in some experiments, other sound techniques like model-checking). If dependent types would accept unsound proofs, the soundness of the entire type system would be compromised to the point of undefined behavior.

The problem is that deductive proofs have so far shown significantly worse scalability than other formal methods, which is why most of formal methods research is looking elsewhere.

If dependent types could be made more flexible, they will be as good as contract systems.

Re: Dynamic type systems are not inherently more open

#259

Post by pron » Mon, Jan 20, 2020, 11:24 AM UTC

Silhouette wrote: post #239

pron wrote: post #223

Earlier quoted context omitted.

> whereas the contracts we're talking about here are usually checked at run time No, they can be checked in many different ways, hence their power. They can be checked "statically", i.e. at compile-time, or dynamically. One approach is sound but requires more effort, while the other is cheap yet unsound -- and there is a spectrum in between the two extremes. > If you're writing a program that is going to control a sa…

No, they can be checked in many different ways, hence their power. Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time. Such programs often use formal methods that precisely use such contracts. Rich type systems (like Idris's) are virtually never used in practice in those cases.…

> Sure, but the more dynamic ones that drift away from what a (good) static type system offers are exactly the ones that aren't amenable to automated proofs and so tend to be checked at run time.

Not really. What contract systems allow you to do is to separate specification from verification. Type systems require that all of your specifications be verified with deductive proofs. This means that some deep properties either require a lot of work (using a type system such as Idris's) or are excluded from the type system at all. Contracts allow you to check a property in unsound ways, too.

As far as correctness is concerned, contracts do everything a type system can, but more flexibly. Type systems, however, have advantages related to tooling and efficient code generation by an AOT compiler.

> This too is an area with a whole spectrum of possibilities, and some of those involve a degree of formal proof of algorithm properties but not a mechanically verified translation of those algorithms into implementation code.

Even when formal proofs are used, the specification is done in a contract system, not a dependent type system.

Re: Dynamic type systems are not inherently more open

#260

Post by ookdatnog » Mon, Jan 20, 2020, 11:29 AM UTC

sparkie wrote: post #212

ookdatnog wrote: post #135

Earlier quoted context omitted.

> Static type systems will typically require you to state the full type of o. This is not the case for languages with support for structural typing (as the article mentions in the appendix), and most modern statically typed languages have some degree of support for abstract interfaces of some sort which also support writing functions with only partially known information about the type. I think one of the core insigh…

The difference between static and dynamic typing isn't about how explicit you are about the assumptions in your code. You can be equivalently explicit in dynamic and static languages. The fundamental difference lies in when you want the types to be verified. In static typing, that is before the program is run. In dynamic typing, that is before the code is executed if you are explicit, or when the code is executed if…

Yes, you're right, it's not about how explicit you are, or even how explicit you have to be. You can write "stringly typed" code in a static language where none of your assumptions are apparent in the type system. Conversely, regardless of your typing discipline, you can be completely explicit about your assumptions just by writing comments.

This fits in a larger point that, in the end, the technical qualities of a language in many ways matter less than the culture surrounding the language. Even Haskell has unsafePerformIO which means that none of its guarantees about referential transparency actually hold, in theory. In practice, the culture of the language ensures that, when you pull in a library, you can be pretty sure that it's not riddled with unsafePerformIO, and you can almost always treat code as if referential transparency is guaranteed.

A language may facilitate certain habits and discourage other habits. I feel that statically typed languages do not force me to be explicit about my assumptions, but they certainly encourage it by providing immediate benefits to doing so (automated reasoning), and through the culture that surrounds these languages.