Safe Zero-cost Coercions for Haskell

5

Safe Zero-cost Coercions for Haskell ☶ pdf haskell dl.acm.org
via SeanTAllen 3 years ago | cached | 5 comments

5

Generative type abstractions – present in Haskell, OCaml, and other languages – are useful concepts to help prevent programmer errors. They serve to create new types that are distinct at compile time but share a run-time representation with some base type. We present a new mechanism that allows for zero-cost conversions between generative type abstractions and their representations, even when such types are deeply nested. We prove type safety in the presence of these conversions and have implemented our work in GHC.

1

brandonbloom 3 years ago | link

I’m excited to see this.

It’s often said that variables have types in static languages, but that values have types in dynamic language. This paper, to me, seems to reconcile these two ideas by saying: values have types, and so do variables. Generally, those types coincide. In the cases where they don’t coincide, it’s useful to consider the gap between the two.
1. 2
  tel edited 3 years ago | link
  Variables and values absolutely have types in static languages… I’m not certain what gap you’re considering.
  
  |- x : A |- y : B ----------------------- |- (x, y) : A * B
  
  There’s an example of both!
  
  The thing being taken advantage of here is that values at different types which share representation can be coerced without expense. This is already the case some of the time as the coercions which occur are simply id annotated with information to make the typechecker happy and are stripped in untyped languages. The problem is with stuff like zs below
  
  newtype Age = Age Int -- Age ~ Int have identical representation x :: Int x = 3 y = Age y = Age x -- this is free zs = [Age] zs = map Age [1..10] -- this is not since we still map the list, even if each step is free.
2. bitemyapp edited 3 years ago | link
  
  [Comment removed by author]
  1. 2
    
    tel 3 years ago | link
    
    I’m not sure I agree with that. Even at runtime values “have types"—that information is not runtime accessible, but type safety theorems wouldn’t be sensible if you couldn’t talk about types at runtime at least outside of the system. Exactly half of their content is that "types don’t change at runtime”! :)
    1. 1
      
      bitemyapp edited 3 years ago | link
      
      http://clojure-doc.org/articles/ecosystem/core_typed/start/introduction_and_motivation.html
      
      Even the Clojure users know better.
      
      We use the term “type” to mean static type and “tag” for runtime tags. Types only exist at compile time and are used by the static type system to model runtime invariants and properties.
      
      I originally learned this from something Harper said.
      
      This is the last I’ll say on it since I don’t want to expose more surface area to downvotes, people don’t care to know what types are at the moment.
      1. 2
        
        tel edited 3 years ago | link
        
        I think this is mere confusion over the word “have”. The types are erased at runtime in the sense that the runtime dynamics cannot inspect the types—in that sense types fail to exist at runtime and values do not “have” them.
        
        On the other hand, types classify dynamics in the sense that type safety ensures that types are preserved. In this sense, dynamic values “have” types and reduction seeks a canonical value representative of that type.