Skip to content
  • Arnaud Spiwack's avatar
    8e0446df
    Linear let and where bindings · 8e0446df
    Arnaud Spiwack authored
    For expediency, the initial implementation of linear types in GHC
    made it so that let and where binders would always be considered
    unrestricted. This was rather unpleasant, and probably a big obstacle
    to adoption. At any rate, this was not how the proposal was designed.
    
    This patch fixes this infelicity. It was surprisingly difficult to
    build, which explains, in part, why it took so long to materialise.
    
    As of this patch, let or where bindings marked with %1 will be
    linear (respectively %p for an arbitrary multiplicity p). Unmarked let
    will infer their multiplicity.
    
    Here is a prototypical example of program that used to be rejected and
    is accepted with this patch:
    
    ```haskell
    f :: A %1 -> B
    g :: B %1 -> C
    
    h :: A %1 -> C
    h x = g y
      where
        y = f x
    ```
    
    Exceptions:
    - Recursive let are unrestricted, as there isn't a clear semantics of
      what a linear recursive binding would be.
    - Destructive lets with lazy bindings are unrestricted, as their
      desugaring isn't linear (see also #23461).
    - (Strict) destructive lets with inferred polymorphic type are
      unrestricted. Because the desugaring isn't linear (See #18461
      down-thread).
    
    Closes #18461 and #18739
    
    Co-authored-by: @jackohughes
    8e0446df
    Linear let and where bindings
    Arnaud Spiwack authored
    For expediency, the initial implementation of linear types in GHC
    made it so that let and where binders would always be considered
    unrestricted. This was rather unpleasant, and probably a big obstacle
    to adoption. At any rate, this was not how the proposal was designed.
    
    This patch fixes this infelicity. It was surprisingly difficult to
    build, which explains, in part, why it took so long to materialise.
    
    As of this patch, let or where bindings marked with %1 will be
    linear (respectively %p for an arbitrary multiplicity p). Unmarked let
    will infer their multiplicity.
    
    Here is a prototypical example of program that used to be rejected and
    is accepted with this patch:
    
    ```haskell
    f :: A %1 -> B
    g :: B %1 -> C
    
    h :: A %1 -> C
    h x = g y
      where
        y = f x
    ```
    
    Exceptions:
    - Recursive let are unrestricted, as there isn't a clear semantics of
      what a linear recursive binding would be.
    - Destructive lets with lazy bindings are unrestricted, as their
      desugaring isn't linear (see also #23461).
    - (Strict) destructive lets with inferred polymorphic type are
      unrestricted. Because the desugaring isn't linear (See #18461
      down-thread).
    
    Closes #18461 and #18739
    
    Co-authored-by: @jackohughes
Loading