Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,390
    • Issues 4,390
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 373
    • Merge Requests 373
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #19193

Closed
Open
Opened Jan 08, 2021 by Arnaud Spiwack@aspiwackDeveloper

Guards should accept linear variables

Motivation

In GHC 9.0, guards in case expressions or equations cannot contain linear variables (see fixes for #18439 (closed) and #19120 (closed)).

The following, for instance, will refuse to typecheck

f1 :: Bool %1 -> Int
f1 x
  | x = 0
  | otherwise = 1

However, guards are “just” another syntax for case and if expressions, where linear variable make perfect sense:

f2 :: Bool %1 -> Int
f2 x = if x then 0 else 1

In principle, at least, it seems reasonable and idiomatic to allow f1, and such functions.

Proposal

The high-level proposal is easily written: make the type-checker aware of when a guard really consumes a value linearly.

But there are many things to understand

  • We must make sure that such linear guards desugar to linear Core (by which I mean: the linter recognises that the code is properly linear). Maybe it is, maybe we may need to tweak it a little. See also #18806 which has similar issues.
  • In pattern guards, we need to make sure that if the guard is linear, the bound variables are correspondingly linear. This is connected to #18738 .
  • Is f3 linear?
    f3 :: Bool %1 -> Int
    f3 x | x = 0
    f3 x | otherwise = 1
    It's very similar to f1. Though it is typechecked and desugared differently. Does it matter in practice? Is this even reasonable to ask in theory? If the answer is no, though, let me note that around me there are people which consider f1 and f3 to be synonymous, and it may be surprising.
  • Is f4 linear?
    f4 :: Bool %1 -> Int
    f4 x | x = 0
    f4 x = 1
    It looks a lot like f3 too. But it is also different in subtle ways. Here again, some will consider f3 and f4 synonymous. But it's not necessarily clear that typechecking f4 as linear is reasonable in practice (I hope it would be though).

I'm probably forgetting other interesting special cases. But the point is: there is some pen-and-paper work to be done to specify what it even means to specify that a guard is linear. It may be easy, it may be hard; I don't know: I really haven't tried yet. The recent Lower your guard paper may offer a framework to think about these things.

(cc @monoidal @rae )

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#19193