Skip to content

Latest commit

 

History

History
209 lines (160 loc) · 9.9 KB

111016.md

File metadata and controls

209 lines (160 loc) · 9.9 KB
Raw

Nov 10, 2016

Hybrid Types, PFPL Ch. 23

Hengchu

Anouncements

  1. I'm up for the next three lectures. Keep sending me questions before class. Earlier is better.

  2. Project demos start after Thanksgiving. Note the schedule on the webpage and the fact that you'll have 1/3 of a lecture to present what you have done on your project to the rest of the class.

  3. The final project itself is (strictly) due Dec 19th at 9AM. Please turn in the write-up for your work as well as any additional materials (Coq proofs, implementations, etc.) via a pull request to the projects directory of the github repo. (Or by email, if you have trouble with git).

Reading list

Here is a video of a talk I gave on Dynamic Typing in GHC at the Compose Conference and the associated paper.

Dynamic Typing in a Statically Typed Language is an old paper that talks about the addition of a "dynamic" type to a statically typed language.

Questions

  • I like Java's up cast, so hybrid typing can be useful no? Bob clearly doesn't like any sort of dynamic typing! Of course Java's type system is a lot more refined than Bob's language, which brings me to my next question,

  • Is there a widely used language for which we can say Bob's language is a faithful representation of? It seems to me that Bob took Java's down cast, which I think is not a good feature, and amplified it's badness. But up casts are very useful, yet I didn't see where Bob mentioned why this might be a feature worth having.

    [SCW: answering these two questions together. It is the case that the "Object" type can work as a dynamic type in Java using (implicit) up casts and explicit, checked downcasts. With this interpretation, we can view Java as an example of a language with a "hybrid" type system.

    However, if you are only interested in up-casts in a language with a trivial subtyping system (i.e. the only subtype relationship allowed is A <: Top) then we already can do similar things with existential types: The type "exists a.a" is a supertype of any type, and doesn't permit any down casting. However, by itself, I don't think this feature is very useful. Java's up casting is good because of its richer subtype hierarchy.]

  • If we disallow down casts then what would be the argument against hybridly typed languages? Also, wouldn't removing down casts make Bob's language type safe (and maybe Java as well)?

    [SCW: I would argue that downcasts are what make a language hybridly typed in the first place. Note that this language (and Java) are type safe. The issue is that the safety theorems must account for failed downcasts. See the FJ paper for more details about what Java's type safety theorem might look like.]

  • Is there any difference between HPCF's "dyn" and Haskell's "Dynamic"? It looks as if the correspondence new[l] <-> toDyn , cast[l] <-> fromDynamic, and inst[l] <-> isJust . fromDynamic @ l, holds if you squint hard enough at the dictionaries/typeclasses. Is there anything I'm missing or are they pretty much the same thing?

    [SCW: They are very close, but there is one key difference. Haskell's Dynamic has more "classes" than HPCF. For example, the only class for functions in HPCF works for Dyn -> Dyn. However, in Haskell you can directly construct a dynamic type from any function type, such as Int -> Int.]

  • I think of dynamic types as sum types. So, loosely speaking, dyn = num + fun. Why not use sum types then?

    [SCW: In a language with a closed set of types, you can just use a recursive datatype.

     data Dyn = Num Int | Fun (Dyn -> Dyn)

    However, once you have newtypes, then you need a mechanism to extend this sum.]

  • In the introductory section, we have "The ad hoc device of adding the type dyn to a static language is unnecessary in a language with recursive types ..." So if a language has recursive types, then there is no necessity of dynamic typing and by extension, hybrid typing?

    [SCW: Yes, with the caveat about newtypes above. Also, there may be additional justification for a special purpose language extension depending on what sort of type inference is available in the language. It is possible, in some contexts, that the coercions to the dynamic type can be inferred, which would make the hybrid system easier to work with.]

  • Section 23.3 ends with something like, "Applying this principle generally, we see that dynamic typing is only of marginal utility --- it is used only at the margins of a system where uncontrolled calls arise. Internally to a system there is no benefit, and considerable drawback, to restricting attention to the type dyn." So is this, in short, saying that, "Well we studied this, but this is almost useless."?

    [SCW: That's Bob for you.]

  • Why Bob says dynamic typing is only of marginal utility? Could you clarify it more?

    [SCW: See above]

  • I wonder how statically typed languages actually implement dynamic types? Do they use recursive types, or other approaches? And if they don’t use recursive types, why?

    [SCW: See the Dynamics in GHC paper above. Or, if recursive types are already available, then there is nothing for the language to do --- it is up to the user to define the dynamic type. Note: there are other mechanisms to implement type Dynamic besides recursive types. ]

  • Many times, Bob emphasizes that "dynamic languages are a mode of use of static languages". Is this true always true of any conceivable dynamic language?

    [SCW: Good question. It is true for the ones that I know. The only requirement is that the "unitype" of the dynamic language be expressible in the static language.]

  • In our list of advantages/disadvantages of typing disciplines, how does hybrid typing compare?

    [SCW: Good question, but probably better addressed by in class discussion.]

  • Are there any stronger properties we could prove about HPCF? I think we'd want to be able to say something about in what contexts err can occur (only when we're dealing with values of type dyn).

    [SCW: This is a property that falls out of the semantics (and indirectly from the safety theorem). You can see that err only results from a failed cast, i.e. rule (23.2e) and doesn't propagate.]

  • How hard is it in practice to perform optimizations like those in 23.3? I ask mostly because the "Is Sound Gradual Typing Dead?" paper at POPL 2016 seems to suggest that it's harder to optimize away these contract checks than you would expect.

    [SCW: link to paper though I haven't yet read it closely. I think that depends on context and programming idioms used in the dynamic language. It also depends on whether this optimization is done via static analysis, or as part of a JIT (where much more information is known).]

  • The optimization seems ad-hoc to me. Is there a well-formed algorithm or a set of rules for transformation?

    [SCW: good question. It partly depends on deducing a loop invariant for the recursive function, which is undecidable in general.]

  • It would be great if you could give some actual examples of hybrid typing in real programming languages.

    [SCW: Java's objects with downcasting. Haskell's type Dynamic. OCaml's type dyn. Many examples via encoding with recursive types.]

  • Could we go over the optimization example together? In particular, it would be nice to see the different terms we obtain at each step (the book is a little too verbose on that part, in my opinion)

  • Could we also talk about the usefulness of dynamic typing? With Bob's brilliantly sharp argument about them being merely a limited subcase of static typing, and since we have sum types in any sensible language*, I just don't see how they can be useful... I don't buy the "they're easier to get right" argument - I mean, why use a buggy interpreter for a terrible dynamically-typed language when one can rely on a verified compiler for a statically-typed one (that could have dependent types (or another mechanism) to represent permissions, so that your browser stays safe)? It seems like we're constraining ourselves to a completely suboptimal technology - and the argument for that doesn't even hold: I am fairly certain that, in any major browser these days, the interpreter for say, javascript, is an awfully complicated piece of software - not only to deal with the intrinsically flawed language, but also to perform (buggy and unsafe) optimizations that allow scripts to be executed with non laughable performance. So really, I still didn't encounter a valid argument in favor of the dynamic typing restriction; I'd be interested to know if anybody has one, or if that could possibly exist.

    • (Heterogeneity is in my opinion the only feature where people think it makes a difference (dyn vs static), alongside type inference)

    [SCW: this is a request to continue our in class discussion from last time. BTW, here is the paper I was referring to last time, when I mentioned that dynamic languages are simpler to implement safely. It is not anti-type systems, but it is a very different model than the one put forth by Bob.]

  • I saw the types and classes in HPCF can be unified with subtyping, advantages of the latter discussed in Ch24.2. So what are the advantages of keep separating these two concepts?

    [SCW: Subtyping has many interactions with type inference, which are ignored in this chapter.]

  • Is there any relation between "types and classes" in HPCF and "kinds and types" in Coq?

    [SCW: Not really. "classes" are really tags for types, so they don't correspond to kinds. Instead the better correspondence is with a data structure in Coq that represent types.]