Commit 5830a12c authored by Vladislav Zavialov's avatar Vladislav Zavialov Committed by Marge Bot
Browse files

New linear types syntax: a %p -> b (#18459)

Implements GHC Proposal #356

Updates the haddock submodule.
parent b31a3360
......@@ -1321,7 +1321,7 @@ dataConStupidTheta dc = dcStupidTheta dc
Note [Displaying linear fields]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
A constructor with a linear field can be written either as
MkT :: a #-> T a (with -XLinearTypes)
MkT :: a %1 -> T a (with -XLinearTypes)
or
MkT :: a -> T a (with -XNoLinearTypes)
......@@ -1330,7 +1330,7 @@ They differ in how linear fields are handled.
1. dataConWrapperType:
The type of the wrapper in Core.
For example, dataConWrapperType for Maybe is a #-> Just a.
For example, dataConWrapperType for Maybe is a %1 -> Just a.
2. dataConNonlinearType:
The type of the constructor, with linear arrows replaced by unrestricted ones.
......
......@@ -216,7 +216,7 @@ That is, in
We have
Just :: a #-> Just a
Just :: a %1 -> Just a
The goal is to maximise reuse of types between linear code and traditional
code. This is argued at length in the proposal and the article (links in Note
......@@ -232,7 +232,7 @@ backwards compatibility. Consider
We have
map :: (a -> b) -> f a -> f b
Just :: a #-> Just a
Just :: a %1 -> Just a
Types don't match, we should get a type error. But this is legal Haskell 98
code! Bad! Bad! Bad!
......@@ -242,7 +242,7 @@ polymorphism.
Instead, we generalise the type of Just, when used as term:
Just :: forall {p}. a #p-> Just a
Just :: forall {p}. a %p-> Just a
This is solely a concern for higher-order code like this: when called fully
applied linear constructors are more general than constructors with unrestricted
......
......@@ -1490,7 +1490,7 @@ pushCoValArg co
-- We can't push the coercion in the case where co_mult isn't reflexivity:
-- it could be an unsafe axiom, and losing this information could yield
-- ill-typed terms. For instance (fun x ::(1) Int -> (fun _ -> () |> co) x)
-- with co :: (Int -> ()) ~ (Int #-> ()), would reduce to (fun x ::(1) Int
-- with co :: (Int -> ()) ~ (Int %1 -> ()), would reduce to (fun x ::(1) Int
-- -> (fun _ ::(Many) Int -> ()) x) which is ill-typed
-- If co :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
......
......@@ -412,7 +412,7 @@ EtaExpansion:
fail = \void. (\s. (e |> g) s) |> sym g where g :: IO () ~ S -> (S,())
--> Next iteration of simplify
fail1 = \void. \s. (e |> g) s
fail = fail1 |> Void#->sym g
fail = fail1 |> Void# -> sym g
And now inline 'fail'
CaseMerge:
......
......@@ -2640,7 +2640,7 @@ rebuildCase env scrut case_bndr alts cont
--
-- As an illustration, consider the following
-- case[Many] case[1] of { C x -> C x } of { C x -> (x, x) }
-- Where C :: A #-> T is linear
-- Where C :: A %1 -> T is linear
-- If we were to produce a case[1], like the inner case, we would get
-- case[1] of { C x -> (x, x) }
-- Which is ill-typed with respect to linearity. So it needs to be a
......
......@@ -953,7 +953,7 @@ adjustJoinPointType mult new_res_ty join_id
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider a join point which is linear in its variable, in some context E:
E[join j :: a #-> a
E[join j :: a %1 -> a
j x = x
in case v of
A -> j 'x'
......@@ -961,7 +961,7 @@ E[join j :: a #-> a
The simplifier changes to:
join j :: a #-> a
join j :: a %1 -> a
j x = E[x]
in case v of
A -> j 'x'
......
......@@ -1342,5 +1342,3 @@ exprIsLambda_maybe (in_scope_set, id_unf) e
exprIsLambda_maybe _ _e
= -- pprTrace "exprIsLambda_maybe:Fail" (vcat [ppr _e])
Nothing
......@@ -1538,7 +1538,7 @@ types of a GADT constructor, since there are some non-obvious details involved.
While splitting the argument types of a record GADT constructor is easy (they
are stored in an HsRecTy), splitting the arguments of a prefix GADT constructor
is trickier. The basic idea is that we must split along the outermost function
arrows ((->) and (#->)) in the type, which GHC.Hs.Type.splitHsFunType
arrows ((->) and (%1 ->)) in the type, which GHC.Hs.Type.splitHsFunType
accomplishes. But what about type operators? Consider:
C :: a :*: b -> a :*: b -> a :+: b
......
......@@ -936,9 +936,9 @@ data HsArrow pass
= HsUnrestrictedArrow
-- ^ a -> b
| HsLinearArrow
-- ^ a #-> b
-- ^ a %1 -> b
| HsExplicitMult (LHsType pass)
-- ^ a # m -> b (very much including `a # Many -> b`! This is how the
-- ^ a %m -> b (very much including `a %Many -> b`! This is how the
-- programmer wrote it). It is stored as an `HsType` so as to preserve the
-- syntax as written in the program.
......
......@@ -280,7 +280,7 @@ Context:
context -> btype .
type -> btype .
type -> btype . '->' ctype
type -> btype . '#->' ctype
type -> btype . '->.' ctype
Example:
a :: Maybe Integer -> Bool
......@@ -636,7 +636,7 @@ are the most common patterns, rewritten as regular expressions for clarity:
'|' { L _ ITvbar }
'<-' { L _ (ITlarrow _) }
'->' { L _ (ITrarrow _) }
'#->' { L _ (ITlolly _) }
'->.' { L _ ITlolly }
TIGHT_INFIX_AT { L _ ITat }
'=>' { L _ (ITdarrow _) }
'-' { L _ ITminus }
......@@ -650,6 +650,7 @@ are the most common patterns, rewritten as regular expressions for clarity:
'>>-' { L _ (ITRarrowtail _) } -- for arrow notation
'.' { L _ ITdot }
PREFIX_AT { L _ ITtypeApp }
PREFIX_PERCENT { L _ ITpercent } -- for linear types
'{' { L _ ITocurly } -- special symbols
'}' { L _ ITccurly }
......@@ -2062,12 +2063,16 @@ type :: { LHsType GhcPs }
>> ams (sLL $1 $> $ HsFunTy noExtField HsUnrestrictedArrow $1 $3)
[mu AnnRarrow $2] }
| btype '#->' ctype {% hintLinear (getLoc $2) >>
ams (sLL $1 $> $ HsFunTy noExtField HsLinearArrow $1 $3)
[mu AnnLolly $2] }
| btype mult '->' ctype {% hintLinear (getLoc $2) >>
ams (sLL $1 $> $ HsFunTy noExtField (unLoc $2) $1 $4)
[mu AnnRarrow $3] }
mult :: { LHsType GhcPs }
: btype { $1 }
| btype '->.' ctype {% hintLinear (getLoc $2) >>
ams (sLL $1 $> $ HsFunTy noExtField HsLinearArrow $1 $3)
[mu AnnLollyU $2] }
mult :: { Located (HsArrow GhcPs) }
: PREFIX_PERCENT atype { sLL $1 $> (mkMultTy $2) }
btype :: { LHsType GhcPs }
: infixtype {% runPV $1 }
......@@ -3823,7 +3828,7 @@ isUnicode (L _ (ITcparenbar iu)) = iu == UnicodeSyntax
isUnicode (L _ (ITopenExpQuote _ iu)) = iu == UnicodeSyntax
isUnicode (L _ (ITcloseQuote iu)) = iu == UnicodeSyntax
isUnicode (L _ (ITstar iu)) = iu == UnicodeSyntax
isUnicode (L _ (ITlolly iu)) = iu == UnicodeSyntax
isUnicode (L _ ITlolly) = True
isUnicode _ = False
hasE :: Located Token -> Bool
......
......@@ -259,8 +259,7 @@ data AnnKeywordId
| AnnLarrow -- ^ '<-'
| AnnLarrowU -- ^ '<-', unicode variant
| AnnLet
| AnnLolly -- ^ '#->'
| AnnLollyU -- ^ '#->', unicode variant
| AnnLollyU -- ^ The '⊸' unicode arrow
| AnnMdo
| AnnMinus -- ^ '-'
| AnnModule
......@@ -364,7 +363,6 @@ unicodeAnn AnnOpenB = AnnOpenBU
unicodeAnn AnnCloseB = AnnCloseBU
unicodeAnn AnnOpenEQ = AnnOpenEQU
unicodeAnn AnnCloseQ = AnnCloseQU
unicodeAnn AnnLolly = AnnLollyU
unicodeAnn ann = ann
......
......@@ -768,14 +768,15 @@ data Token
| ITvbar
| ITlarrow IsUnicodeSyntax
| ITrarrow IsUnicodeSyntax
| ITlolly IsUnicodeSyntax
| ITdarrow IsUnicodeSyntax
| ITlolly -- The (⊸) arrow (for LinearTypes)
| ITminus -- See Note [Minus tokens]
| ITprefixminus -- See Note [Minus tokens]
| ITbang -- Prefix (!) only, e.g. f !x = rhs
| ITtilde -- Prefix (~) only, e.g. f ~x = rhs
| ITat -- Tight infix (@) only, e.g. f x@pat = rhs
| ITtypeApp -- Prefix (@) only, e.g. f @t
| ITpercent -- Prefix (%) only, e.g. a %1 -> b
| ITstar IsUnicodeSyntax
| ITdot
......@@ -1024,8 +1025,7 @@ reservedSymsFM = listToUFM $
,("→", ITrarrow UnicodeSyntax, UnicodeSyntax, 0 )
,("←", ITlarrow UnicodeSyntax, UnicodeSyntax, 0 )
,("#->", ITlolly NormalSyntax, NormalSyntax, 0)
,("⊸", ITlolly UnicodeSyntax, UnicodeSyntax, 0)
,("⊸", ITlolly, UnicodeSyntax, 0)
,("⤙", ITlarrowtail UnicodeSyntax, UnicodeSyntax, xbit ArrowsBit)
,("⤚", ITrarrowtail UnicodeSyntax, UnicodeSyntax, xbit ArrowsBit)
......@@ -1577,6 +1577,8 @@ varsym_prefix :: Action
varsym_prefix = sym $ \exts s ->
if | s == fsLit "@" -- regardless of TypeApplications for better error messages
-> return ITtypeApp
| LinearTypesBit `xtest` exts, s == fsLit "%"
-> return ITpercent
| ThQuotesBit `xtest` exts, s == fsLit "$"
-> return ITdollar
| ThQuotesBit `xtest` exts, s == fsLit "$$"
......
......@@ -70,6 +70,7 @@ module GHC.Parser.PostProcess (
addFatalError, hintBangPat,
mkBangTy,
UnpackednessPragma(..),
mkMultTy,
-- Help with processing exports
ImpExpSubSpec(..),
......@@ -661,7 +662,7 @@ mkConDeclH98 name mb_forall mb_cxt args
--
-- * If -XLinearTypes is not enabled, the function arrows in a prefix GADT
-- constructor are always interpreted as linear. If -XLinearTypes is enabled,
-- we faithfully record whether -> or #-> was used.
-- we faithfully record whether -> or %1 -> was used.
mkGadtDecl :: [Located RdrName]
-> LHsType GhcPs
-> P (ConDecl GhcPs)
......@@ -2875,6 +2876,10 @@ mkLHsOpTy x op y =
let loc = getLoc x `combineSrcSpans` getLoc op `combineSrcSpans` getLoc y
in L loc (mkHsOpTy x op y)
mkMultTy :: LHsType GhcPs -> HsArrow GhcPs
mkMultTy (L _ (HsTyLit _ (HsNumTy _ 1))) = HsLinearArrow
mkMultTy t = HsExplicitMult t
-----------------------------------------------------------------------------
-- Token symbols
......
......@@ -398,11 +398,11 @@ Projections of records can't be linear:
If we had
a :: Foo #-> A
a :: Foo %1 -> A
We could write
bad :: A #-> B #-> A
bad :: A %1 -> B %1 -> A
bad x y = a (MkFoo { a=x, b=y })
There is an exception: if `b` (more generally all the fields besides `a`) is
......@@ -411,7 +411,7 @@ linear projection has as simple definition.
data Bar = MkBar { c :: C, d # Many :: D }
c :: Bar #-> C
c :: Bar %1 -> C
c MkBar{ c=x, d=_} = x
The `# Many` syntax, for records, does not exist yet. But there is one important
......
......@@ -654,7 +654,7 @@ lparen, rparen, lbrack, rbrack, lbrace, rbrace, blankLine :: SDoc
blankLine = docToSDoc $ Pretty.text ""
dcolon = unicodeSyntax (char '∷') (docToSDoc $ Pretty.text "::")
arrow = unicodeSyntax (char '→') (docToSDoc $ Pretty.text "->")
lollipop = unicodeSyntax (char '⊸') (docToSDoc $ Pretty.text "#->")
lollipop = unicodeSyntax (char '⊸') (docToSDoc $ Pretty.text "%1 ->")
larrow = unicodeSyntax (char '←') (docToSDoc $ Pretty.text "<-")
darrow = unicodeSyntax (char '⇒') (docToSDoc $ Pretty.text "=>")
arrowt = unicodeSyntax (char '⤚') (docToSDoc $ Pretty.text ">-")
......
......@@ -11,7 +11,7 @@ Highlights
----------
* The :extension:`LinearTypes` extension enables linear function syntax
``a #-> b``, as described in the `Linear Types GHC proposal
``a %1 -> b``, as described in the `Linear Types GHC proposal
<https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0111-linear-types.rst>`__.
The GADT syntax can be used to define data types with linear and nonlinear fields.
......
......@@ -6,8 +6,8 @@ Linear types
:since: 9.0.1
Enable the linear arrow ``a #-> b`` and the multiplicity-polymorphic arrow
``a # m -> b``.
Enable the linear arrow ``a %1 -> b`` and the multiplicity-polymorphic arrow
``a %m -> b``.
**This extension is currently considered experimental, expect bugs,
warts, and bad error messages; everything down to the syntax is
......@@ -29,30 +29,28 @@ means that in every branch of the definition of ``f``, its argument
* Calling it as a function and using the result exactly once in the same
fashion.
With ``-XLinearTypes``, you can write ``f :: a #-> b`` to mean that
With ``-XLinearTypes``, you can write ``f :: a %1 -> b`` to mean that
``f`` is a linear function from ``a`` to ``b``. If
:extension:`UnicodeSyntax` is enabled, the ``#->`` arrow can be
:extension:`UnicodeSyntax` is enabled, the ``%1 ->`` arrow can be
written as ``⊸``.
To allow uniform handling of linear ``a #-> b`` and unrestricted ``a
-> b`` functions, there is a new function type ``a # m -> b``. This
syntax is, however, not implemented yet, see
:ref:`linear-types-limitations`. Here, ``m`` is a type of new kind
``Multiplicity``. We have:
To allow uniform handling of linear ``a %1 -> b`` and unrestricted ``a
-> b`` functions, there is a new function type ``a %m -> b``.
Here, ``m`` is a type of new kind ``Multiplicity``. We have:
::
data Multiplicity = One | Many -- Defined in GHC.Types
type a #-> b = a # 'One -> b
type a -> b = a # 'Many -> b
type a %1 -> b = a %One -> b
type a -> b = a %Many -> b
(See :ref:`promotion`).
We say that a variable whose multiplicity constraint is ``Many`` is
*unrestricted*.
The multiplicity-polymorphic arrow ``a # m -> b`` is available in a prefix
The multiplicity-polymorphic arrow ``a %m -> b`` is available in a prefix
version as ``GHC.Exts.FUN m a b``, which can be applied
partially. See, however :ref:`linear-types-limitations`.
......@@ -74,14 +72,14 @@ the value ``MkT1 x`` can be constructed and deconstructed in a linear context:
::
construct :: a #-> MkT1 a
construct :: a %1 -> MkT1 a
construct x = MkT1 x
deconstruct :: MkT1 a #-> a
deconstruct :: MkT1 a %1 -> a
deconstruct (MkT1 x) = x -- must consume `x` exactly once
When used as a value, ``MkT1`` is given a multiplicity-polymorphic
type: ``MkT1 :: forall {m} a. a # m -> T1 a``. This makes it possible
type: ``MkT1 :: forall {m} a. a %m -> T1 a``. This makes it possible
to use ``MkT1`` in higher order functions. The additional multiplicity
argument ``m`` is marked as inferred (see
:ref:`inferred-vs-specified`), so that there is no conflict with
......@@ -103,7 +101,7 @@ Whether a data constructor field is linear or not can be customized using the GA
::
data T2 a b c where
MkT2 :: a -> b #-> c #-> T2 a b -- Note unrestricted arrow in the first argument
MkT2 :: a -> b %1 -> c %1 -> T2 a b -- Note unrestricted arrow in the first argument
the value ``MkT2 x y z`` can be constructed only if ``x`` is
unrestricted. On the other hand, a linear function which is matching
......@@ -124,7 +122,7 @@ Printing multiplicity-polymorphic types
If :extension:`LinearTypes` is disabled, multiplicity variables in types are defaulted
to ``Many`` when printing, in the same manner as described in :ref:`printing-levity-polymorphic-types`.
In other words, without :extension:`LinearTypes`, multiplicity-polymorphic functions
``a # m -> b`` are printed as normal Haskell2010 functions ``a -> b``. This allows
``a %m -> b`` are printed as normal Haskell2010 functions ``a -> b``. This allows
existing libraries to be generalized to linear types in a backwards-compatible
manner; the general types are visible only if the user has enabled
:extension:`LinearTypes`.
......@@ -141,22 +139,20 @@ limitations. If you have read the full design in the proposal (see
:ref:`linear-types-references` below), here is a run down of the
missing pieces.
- The syntax ``a # p -> b`` is not yet implemented. You can use ``GHC.Exts.FUN
p a b`` instead. However, be aware of the next point.
- Multiplicity polymorphism is incomplete and experimental. You may
have success using it, or you may not. Expect it to be really unreliable.
- There is currently no support for multiplicity annotations such as
``x :: a # p``, ``\(x :: a # p) -> ...``.
``x :: a %p``, ``\(x :: a %p) -> ...``.
- All ``case``, ``let`` and ``where`` statements consume their
right-hand side, or scrutiny, ``Many`` times. That is, the following
will not type check:
::
g :: A #-> (A, B)
h :: A #-> B #-> C
g :: A %1 -> (A, B)
h :: A %1 -> B %1 -> C
f :: A #-> C
f :: A %1 -> C
f x =
case g x of
(y, z) -> h y z
......@@ -166,13 +162,13 @@ missing pieces.
::
g :: A #-> (A, B)
h :: A #-> B #-> C
g :: A %1 -> (A, B)
h :: A %1 -> B %1 -> C
f :: A #-> C
f :: A %1 -> C
f x = f' (g x)
where
f' :: (A, B) #-> C
f' :: (A, B) %1 -> C
f' (y, z) = h y z
- There is no support for linear pattern synonyms.
- ``@``-patterns and view patterns are not linear.
......
......@@ -311,7 +311,7 @@ instance Ord (TypeRep a) where
-- | A non-indexed type representation.
data SomeTypeRep where
SomeTypeRep :: forall k (a :: k). !(TypeRep a) #-> SomeTypeRep
SomeTypeRep :: forall k (a :: k). !(TypeRep a) %1 -> SomeTypeRep
instance Eq SomeTypeRep where
SomeTypeRep a == SomeTypeRep b =
......@@ -461,9 +461,9 @@ pattern App f x <- (splitApp -> IsApp f x)
data AppOrCon (a :: k) where
IsApp :: forall k k' (f :: k' -> k) (x :: k'). ()
=> TypeRep f #-> TypeRep x #-> AppOrCon (f x)
=> TypeRep f %1 -> TypeRep x %1 -> AppOrCon (f x)
-- See Note [Con evidence]
IsCon :: IsApplication a ~ "" => TyCon #-> [SomeTypeRep] #-> AppOrCon a
IsCon :: IsApplication a ~ "" => TyCon %1 -> [SomeTypeRep] %1 -> AppOrCon a
type family IsApplication (x :: k) :: Symbol where
IsApplication (_ _) = "An error message about this unifying with \"\" "
......@@ -640,7 +640,7 @@ unkindedTypeRep (SomeKindedTypeRep x) = SomeTypeRep x
data SomeKindedTypeRep k where
SomeKindedTypeRep :: forall k (a :: k). TypeRep a
#-> SomeKindedTypeRep k
%1 -> SomeKindedTypeRep k
kApp :: SomeKindedTypeRep (k -> k')
-> SomeKindedTypeRep k
......@@ -730,7 +730,7 @@ bareArrow (TrFun _ m a b) =
bareArrow _ = error "Data.Typeable.Internal.bareArrow: impossible"
data IsTYPE (a :: Type) where
IsTYPE :: forall (r :: RuntimeRep). TypeRep r #-> IsTYPE (TYPE r)
IsTYPE :: forall (r :: RuntimeRep). TypeRep r %1 -> IsTYPE (TYPE r)
-- | Is a type of the form @TYPE rep@?
isTYPE :: TypeRep (a :: Type) -> Maybe (IsTYPE a)
......
......@@ -820,10 +820,10 @@ So we always print a SigT with parens (see #10050). -}
pprTyApp :: (Type, [TypeArg]) -> Doc
pprTyApp (MulArrowT, [TANormal (PromotedT c), TANormal arg1, TANormal arg2])
| c == oneName = sep [pprFunArgType arg1 <+> text "#->", ppr arg2]
| c == oneName = sep [pprFunArgType arg1 <+> text "%1 ->", ppr arg2]
| c == manyName = sep [pprFunArgType arg1 <+> text "->", ppr arg2]
pprTyApp (MulArrowT, [TANormal argm, TANormal arg1, TANormal arg2]) =
sep [pprFunArgType arg1 <+> text "#" <+> ppr argm <+> text "->", ppr arg2]
sep [pprFunArgType arg1 <+> text "%" <> ppr argm <+> text "->", ppr arg2]
pprTyApp (ArrowT, [TANormal arg1, TANormal arg2]) = sep [pprFunArgType arg1 <+> text "->", ppr arg2]
pprTyApp (EqualityT, [TANormal arg1, TANormal arg2]) =
sep [pprFunArgType arg1 <+> text "~", ppr arg2]
......
......@@ -2,8 +2,8 @@
module Linear1Rule where
-- Test the 1 <= p rule
f :: a #-> b
f :: a %1 -> b
f = f
g :: a # p -> b
g :: a %p -> b
g x = f x
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment