Just as a reminder to myself: the BndrMap
type will need to change for this too.
Currently, it's a trie on (Type, Mult)
, and it will need to be a trie on (Type, IdBinding)
. Let me not forget this.
The syntax (->) isn't really a name at all -- it's just a slice of syntax.
I don't think that's true anymore, now that linear types have landed. It's merely wired in. But it's also not very relevant anymore, since the bug now concerns FUN
and TYPE
only.
Maybe just kill off that module qualification without talking about
BuiltInSyntax
.
I remember there being a way to do that. Declare an identifier as always in scope. I've done that for One
and Many
.
It would be fair to start with LetBound
containing no data. As soon as lint doesn't panic, then we have, at least, properly classified let-bound and lambda-bound variables. Adding the usage environment of whatever equivalent structure would then be fairly routine, I think.
Kill the comment: it's obsolete. This is fully replaced by seq_id_ty = idType seqId
above. Which is basically what this comment was about: we needed to synchronise the multiplicity, there, with the type of seq
. Now, we don't.
One fewer complexity: good.
Ah no, that wasn't the intent. I wrote it as a pretend data type for the sake of what I hoped was clarity, but ended up being confusion. The idea was that Unrestricted#
is exactly the same thing as a one-argument unboxed tuple, but for the type.
It's an accurate summary yes.
With the understanding that scaling a usage environment by Many
will leave it with only 0
-s and Many
-s. So if a bottoming expression is passed to a function which requires an unrestricted argument, it will, essentially, only have an environment composed of Many
-s, and will leave the linear variables alone.
I've got to admit that I'm not completely sure what your point is. However:
const
can't be linear in its second argumentcase {}
in a non-linear position can't consume linear variables (if the type checker lets it: it's a bug)f x = outOfScope
will type-check. And return an error at run time. This behaviour is correct: errors are allowed to consume linear variables arbitrary many times.Since I'm shooting in the dark, I don't know if the above points answer your concerns. So let me know.
The alternative has an impact on runtime, and that makes me unhappy.
Does it? I've always expected case x of { (# x, y #) -> … }
to be a no-op in the runtime. But I guess I was mistaken.
This seems to advocate for the alternative solution, which would be a touch annoying to deploy, as we would have to replace a single case expression by multiple nested expressions. But could be hacked together more locally.
I'm not sure it's really what we want to do. So honestly, maybe there is cause for debate and design here.
Writing a typed hole with linear arguments in scope gives spurious linearity errors. It does not help that these errors are display first, so that in ghcid, for instance, we may not even be able see the type of the hole.
{-# LANGUAGE LinearTypes #-}
f :: Int #-> Bool #-> Char
f x y = _
Raises the following error:
<interactive>:15:31: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘x’
• In an equation for ‘f’: f x y = _
<interactive>:15:33: error:
• Couldn't match type ‘'Many’ with ‘'One’
arising from multiplicity of ‘y’
• In an equation for ‘f’: f x y = _
<interactive>:15:37: error:
• Found hole: _ :: Char
• In the expression: _
In an equation for ‘f’: f x y = _
• Relevant bindings include
y :: Bool (bound at <interactive>:15:33)
x :: Int (bound at <interactive>:15:31)
f :: Int #-> Bool #-> Char (bound at <interactive>:15:29)
Valid hole fits include
maxBound :: forall a. Bounded a => a
with maxBound @Char
(imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))
minBound :: forall a. Bounded a => a
with minBound @Char
(imported from ‘Prelude’ (and originally defined in ‘GHC.Enum’))
Notice the two multiplicity errors at the top. Which are caused by the fact that the typechecker considers that _
counts for 0 use of x
and y
(where it ought to be: an unknown number of uses).
Contrast the behaviour of _
with the behaviour of an empty case:
f :: Int #-> Bool #-> Char
f x y = () & \case {}
This compiles without a type error.
So holes should treat multiplicities exactly how a case {}
would. After all, it's more or less the same idea: _
uses x
and y
an unknown number of times, and \case {}
consumes x
and y
an arbitrary number of times. Since we don't know how many x
-s and y
-s are in _
, we don't want to complain about it, so it's natural to approximate _
to be consuming x
and y
an arbitrary number of times.
Currently, an unboxed tuple always have all fields linear. This is fine for most purpose but it actually does hamper optimisations. This is a problem which only happens on code using -XLinearTypes
, therefore it's not too serious, but still we ought to make good by it.
Specifically, it concerns the CPR transformation when the returned argument has an unrestricted field (e.g. the Unrestricted
datatype which has a single unrestricted field). The story is expounded in the wiki page. Let me copy the explanation here.
Consider a function
f :: Int -> Unrestricted A
The argument type doesn't matter, the result type does.
The CPR split yields:
$wf :: Int -> (# A #)
f x = case_1 $wf x of
(# y #) -> Unrestricted y
This is ill-typed unless (# #)
has an unrestricted field (currently, all fields of an unboxed tuple are linear).
Therefore, CPR is restricted to the case where the constructor only has linear field.
To be able to activate the CPR worker/wrapper split on data types with an unrestricted field, unboxed tuple should be parametrised by the multiplicity of their field, that is
type (#,#) :: forall r s. Multiplicity -> Multiplicity -> TYPE r -> TYPE s -> TYPE …
data (#,#) p q a b where
(#,#) :: a #p-> b #q-> (#,#) p q a b
At least the unboxed tuples used by Core should have such a type. It can also be a user-facing feature.
An alternative is to have a single additional unboxed data type
data Unrestricted# a where
Unrestricted# :: a -> Unrestricted# a -- unrestricted field
And we could use (# a, Unrestricted# b #)
in CPR as the unboxed stand in for a data type which is linear in its first field and unrestricted in its second field.
I don't know either. I'd imagine it's fairly easy. But if it turns out not to be, an alternative, indeed, could be to disallow linear types in FFI function. It would be a type-checking error.
You are right about Double
, indeed. There is no difference between a linear C Double
(let's say Double#
) function and an unrestricted Double#
function. But we can certainly cook up more complex situations. For instance, I may pass a thunk to C, and it may fail to return it to me. Or I may pass a Haskell function to C and it fails to apply it to something, or applies it more than once.
So it's not a given that FFI functions are linear.
I'd say: exactly as pure (as in not effectful) FFI calls. Namely: don't get it wrong. I don't see any reason why purity and linearity would be different, in that respect. Unless I'm missing something, of course.
The desugaring of FFI-defined functions drops linearity information.
The following module
{-# LANGUAGE LinearTypes #-}
module II where
foreign import ccall "exp" c_exp :: Double #-> Double
fails linear lint:
*** Core Lint errors : in result of Desugar (before optimization) ***
II.hs:4:1: warning:
Linearity failure in lambda: ds_du1
'Many ⊈ 'One
In the RHS of c_exp :: Double #-> Double
In the body of lambda with binder ds_du1 :: Double
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
II.hs:4:1: warning:
Linearity failure in lambda: ds_du1
'Many ⊈ 'One
In the RHS of c_exp :: Double #-> Double
In the unfolding of c_exp :: Double #-> Double
In the body of lambda with binder ds_du1 :: Double
Substitution: [TCvSubst
In scope: InScope {}
Type env: []
Co env: []]
*** Offending Program ***
Rec {
$wccall_du7
:: Double# -> State# RealWorld -> (# State# RealWorld, Double# #)
[LclId]
$wccall_du7
= \ (ds_du3 :: Double#) ->
{__pkg_ccall_GC main Double#
-> State# RealWorld -> (# State# RealWorld, Double# #)}_du6
ds_du3
c_exp :: Double #-> Double
[LclIdX,
Unf=Unf{Src=InlineStable, TopLvl=True, Value=True, ConLike=True,
WorkFree=True, Expandable=True,
Guidance=ALWAYS_IF(arity=1,unsat_ok=False,boring_ok=False)
Tmpl= \ (ds_du1 [Occ=Once!] :: Double) ->
case ds_du1 of { D# ds_du3 [Occ=Once] ->
case $wccall_du7 ds_du3 realWorld# of
{ (# _ [Occ=Dead], ds_du4 [Occ=Once] #) ->
D# ds_du4
}
}}]
c_exp
= (\ (ds_du1 :: Double) ->
case ds_du1 of ds_du2 { D# ds_du3 ->
case $wccall_du7 ds_du3 realWorld# of wild_00
{ (# ds_du5, ds_du4 #) ->
D# ds_du4
}
})
`cast` (<Double #-> Double>_R
:: (Double #-> Double) ~R# (Double #-> Double))
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "II"#)
end Rec }
*** End of Offense ***
Linear FFI functions are perfectly reasonable a thing to have. So we should desugar them properly. This was actually spotted in review: !852 (diffs) . It's a matter of pushing the information until this spot.
Since !852 was merged, the case
expression in the Core definition of constructor wrappers are linear cases.
data T = MkT !Int
Will have a wrapper along the lines of
$WT n = case n of n' # 1
_ -> MkT n'
Now, as explained in the wiki, having a case[One]
prevents binder-swap from happening. And, as it happens, we have seen examples of Core getting less optimised because of it. I don't remember the precise example, unfortunately, but it concerned a cascade of such workers inlined into one-another, and some case-of-case not happening (probably unsurprisingly as this is very much the sort of things that binder-swap is here to detect).
It doesn't really show in any tests, but it does make some non-linear code a bit less optimised. And that's rather unfortunate.
My suggestion is to add, as part of occurrence analysis, a new transformation. This transformation would detect cases where the scrutinee is really unrestricted, and change the case[One]
into a case[Many]
.
The point is that: if case[Many]
is still well typed, then we have strictly more freedom for optimisation.
The question remains of how we can detect that case[One]
can be promoted to case[Many]
. My proposal is to do so if and only if the scrutinee is a variable and this variable is bound with multiplicity Many
.
When I say
{-# LANGUAGE TemplateHaskell, LinearTypes #-}
module Bug where
import Language.Haskell.TH
f :: Q Exp ->. Q Exp
f x = [| Just $x |]
I get
*** Core Lint errors : in result of Desugar (before optimization) ***
Bug.hs:8:3: warning:
[in body of lambda with binder x_a8Ki :: Q Exp]
Linearity failure in lambda: x_a8Ki
'Omega ⊈ 'One
*** Offending Program ***
Rec {
$trModule :: Module
[LclIdX]
$trModule = Module (TrNameS "main"#) (TrNameS "Bug"#)
f :: Q Exp ->. Q Exp
[LclIdX]
f = \ (x_a8Ki :: Q Exp) ->
break<0>()
appE
(conE
(mkNameG_d
(unpackCString# "base"#)
(unpackCString# "GHC.Maybe"#)
(unpackCString# "Just"#)))
x_a8Ki
end Rec }
*** End of Offense ***
The problem is that Template Haskell slices desugars to calls to appE
, conE
, etc… which are not linear functions (and probably oughtn't be anyway). Consequently, slices should not be considered linear in their antiquoted positions.
It is probably sufficient to call tcScalingUsage Many
in
tcPendingSplice
tcTypedBracket
tcUntypedBracket
around the calls to tcMonoExpr
and tcInferRhoNC
.The linear types proposal describes how to extend the multiplicity annotations as in #18460 and #18461 to control the multiplicity of record fields.
The syntax is
data R = R { unrestrictedField # 'Many :: A, linearField # 'One :: B }
I imagine the difficulty will be similar as in #18461 . A lot of places will simply be assuming that records have fields of multiplicity One
. Though I'm a bit hopeful that we may mostly just need to follow the typechecker on this one.
This is a continuation of #18460 : we want to support the multiplicity annotation on let
and where
binders.
let x # p = … in …
let x # p :: a = … in …
See the linear types proposal for more.
There is quite a bit of work here. That's why I made it a separate issue of #18460 . There are a number of shortcuts in the code where we simply assume that let
binders have multiplicity Many
. Since there is no way to make them otherwise. And even if we had been careful to not make such assumptions, the fact that all let
binders are indeed Many
means that the code would probably be incorrect.
The linear types proposal introduces a syntax to annotate a lambda binder (or more generally a pattern) with a multiplicity, when -XScopedTypeVarialbes
is on (that is, whenever a type annotation is allowed).
The syntax is
\ x # p -> …
\ x # p :: a -> …
This is, I believe, fully specified by the following type annotation grammar rule for pattern:
pat -> pat [# btype] [:: type]
I expect that a lot of the necessary material is there already. This does change the typechecking algorithm a little, which will now have the ability to generate linear functions outside of checking mode.
In this issue, I suggest that we make annotating let expression thus an error. As it's a harder issue. I've made it #18461 .