Adds a linear fat arrow %1 => this is meant to greatly improve the ergonomics of some of the APIs using linear types (it tends to apply to APIs based on typestate or related to mutation).

Rendered

  • MangoIV@functional.cafe
    link
    fedilink
    arrow-up
    1
    ·
    1 year ago

    @jaror will this interact with any future proposals towards DH? I’m worried that this increase the pile of chores one would have to do to finally reach the goal of implementing them, similarly to how it happened with LinearTypes (and multiplicity polymorphism ftm) themselves.

    • jaror@kbin.socialOP
      link
      fedilink
      arrow-up
      1
      ·
      1 year ago

      The changes seem pretty modest as the costs and drawbacks section also says. But I wouldn’t know how complicated it is to combine normal constraints with dependent types, let alone linear constraints.

      • MangoIV@functional.cafe
        link
        fedilink
        arrow-up
        1
        ·
        1 year ago

        @jaror yeah it seems fine at first; issue is that someone probably has to do the theory part, writing a new papers for every one new addition seems tedious 😅