[Git][ghc/ghc][wip/marge_bot_batch_merge_job] 2 commits: Drop hard Xcode dependency
Marge Bot (@marge-bot)
gitlab at gitlab.haskell.org
Tue Dec 12 22:00:59 UTC 2023
Marge Bot pushed to branch wip/marge_bot_batch_merge_job at Glasgow Haskell Compiler / GHC
Commits:
2551c2d6 by Moritz Angermann at 2023-12-12T17:00:52-05:00
Drop hard Xcode dependency
XCODE_VERSION calls out to `xcodebuild`, which is only available
when having `Xcode` installed. The CommandLineTools are not
sufficient. To install Xcode, you must have an apple id to download
the Xcode.xip from apple.
We do not use xcodebuild anywhere in our build explicilty. At best
it appears to be a proxy for checking the linker or the compiler.
These should rather be done with
```
xcrun ld -version
```
or similar, and not by proxy through Xcode. The CLR should be
sufficient for building software on macOS.
- - - - -
c9e17a97 by Vladislav Zavialov at 2023-12-12T17:00:52-05:00
docs: update information on RequiredTypeArguments
Update the User's Guide and Release Notes to account for the recent
progress in the implementation of RequiredTypeArguments.
- - - - -
6 changed files:
- configure.ac
- distrib/configure.ac.in
- docs/users_guide/9.10.1-notes.rst
- docs/users_guide/exts/required_type_arguments.rst
- docs/users_guide/using-warnings.rst
- − m4/xcode_version.m4
Changes:
=====================================
configure.ac
=====================================
@@ -342,9 +342,6 @@ then
GMP_FORCE_INTREE="YES"
fi
-XCODE_VERSION()
-
-
dnl ** Building a cross compiler?
dnl --------------------------------------------------------------
CrossCompiling=NO
=====================================
distrib/configure.ac.in
=====================================
@@ -94,8 +94,6 @@ then
AC_MSG_ERROR([find is required.])
fi
-XCODE_VERSION()
-
AC_ARG_ENABLE(distro-toolchain,
[AS_HELP_STRING([--enable-distro-toolchain],
[Do not use bundled Windows toolchain binaries.])],
=====================================
docs/users_guide/9.10.1-notes.rst
=====================================
@@ -6,17 +6,34 @@ Version 9.10.1
Language
~~~~~~~~
-- Part 1 of GHC Proposal `#281
- <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
- "Visible forall in types of terms" has been implemented.
+- GHC Proposal `#281 <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0281-visible-forall.rst>`_
+ "Visible forall in types of terms" has been partially implemented.
The following code is now accepted by GHC::
- idv :: forall a -> a -> a
- idv (type a) (x :: a) = x
+ {-# LANGUAGE RequiredTypeArguments #-}
- x = idv (type Int) 42
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
+
+ s1 = vshow Int 42 -- "42"
+ s2 = vshow Double 42 -- "42.0"
+
+ The use of ``forall a ->`` instead of ``forall a.`` indicates a *required* type
+ argument. A required type argument is visually indistinguishable from a value
+ argument but does not exist at runtime.
+
+ This feature is guarded behind :extension:`RequiredTypeArguments`.
+
+- The :extension:`ExplicitNamespaces` extension can now be used in conjunction
+ with :extension:`RequiredTypeArguments` to select the type namespace in a
+ required type argument::
+
+ data T = T -- the name `T` is ambiguous
+ f :: forall a -> ... -- `f` expects a required type argument
+
+ x1 = f T -- refers to the /data/ constructor `T`
+ x2 = f (type T) -- refers to the /type/ constructor `T`
- This feature is guarded behind :extension:`RequiredTypeArguments` and :extension:`ExplicitNamespaces`.
- With :extension:`LinearTypes`, ``let`` and ``where`` bindings can
now be linear. So the following now typechecks::
@@ -28,7 +45,6 @@ Language
where
y = f x
-
- Due to an oversight, previous GHC releases (starting from 9.4) allowed the use
of promoted data types in kinds, even when :extension:`DataKinds` was not
enabled. That is, GHC would erroneously accept the following code: ::
=====================================
docs/users_guide/exts/required_type_arguments.rst
=====================================
@@ -19,42 +19,94 @@ dependent quantification in types of terms::
id :: forall a. a -> a -- invisible dependent quantification
id_vdq :: forall a -> a -> a -- visible dependent quantification
-Note that the arrow in ``forall a ->`` is part of the syntax and not a function
-arrow, just like the dot in ``forall a.`` is not a type operator. The essence of
-a ``forall`` is the same regardless of whether it is followed by a dot or an
-arrow: it introduces a type variable. But the way we bind and specify this type
-variable at the term level differs.
+The arrow in ``forall a ->`` is part of the syntax and not a function arrow,
+just like the dot in ``forall a.`` is not a type operator.
-When we define ``id``, we can use a lambda to bind a variable that stands for
-the function argument::
+The choice between ``forall a.`` and ``forall a ->`` does not have any effect on
+program execution. Both quantifiers introduce type variables, which are erased
+during compilation. Rather, the main difference is in the syntax used at call
+sites::
- -- For reference: id :: forall a. a -> a
- id = \x -> x
+ x1 = id True -- invisible forall, the type argument is inferred by GHC
+ x2 = id @Bool True -- invisible forall, the type argument is supplied by the programmer
-At the same time, there is no mention of ``a`` in this definition at all. It is
-bound by the compiler behind the scenes, and that is why we call the ordinary
-``forall a.`` an *invisible* quantifier. Compare that to ``forall a ->``, which
-is considered *visible*::
+ x3 = id_vdq _ True -- visible forall, the type argument is inferred by GHC
+ x4 = id_vdq Bool True -- visible forall, the type argument is supplied by the programmer
- -- For reference: id_vdq :: forall a -> a -> a
- id_vdq = \(type t) x -> x
+.. _dependent-quantifier:
-This time we have two binders in the lambda:
-* ``type t``, corresponding to ``forall a ->`` in the signature
-* ``x``, corresponding to ``a ->`` in the signature
+Terminology: Dependent quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are said to be "dependent" because the
+result type depends on the supplied type argument: ::
+
+ id @Integer :: Integer -> Integer
+ id @String :: String -> String
+
+ id_vdq Integer :: Integer -> Integer
+ id_vdq String :: String -> String
+
+Notice how the RHS of the signature is influenced by the LHS.
+
+This is in contrast to the function arrow ``->``, which is a non-dependent
+quantifier::
+
+ putStrLn "Hello" :: IO ()
+ putStrLn "World" :: IO ()
+
+The type of ``putStrLn`` is ``String -> IO ()``. No matter what string we pass
+as input, the result type ``IO ()`` does not depend on it.
+
+This notion of dependence is weaker than the one used in dependently-typed
+languages (see :ref:`pi-types`).
+
+Terminology: Visible quantifier
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+We say that ``forall a.`` is an *invisible* quantifier and ``forall a ->`` is a
+*visible* quantifier. This notion of "visibility" is unrelated to implicit
+quantification, which happens when the quantifier is omitted: ::
-And of course, now we also have the option of using the bound ``t`` in a
-subsequent pattern, as well as on the right-hand side of the lambda::
+ id :: a -> a -- implicit quantification, invisible forall
+ id :: forall a. a -> a -- explicit quantification, invisible forall
+ id_vdq :: forall a -> a -> a -- explicit quantification, visible forall
- -- For reference: id_vdq :: forall a -> a -> a
- id_vdq = \(type t) (x :: t) -> x :: t
- -- ↑ ↑ ↑
- -- bound used used
+The property of "visibility" actually describes whether the corresponding type
+argument is visible at the definition site and at call sites: ::
-At use sites, we also instantiate this type variable explicitly::
+ -- Invisible quantification
+ id :: forall a. a -> a
+ id x = x -- defn site: `a` is not mentioned
+ call_id = id True -- call site: `a` is invisibly instantiated to `Bool`
- n = id_vdq (type Integer) 42
- s = id_vdq (type String) "Hello"
+ -- Visible quantification
+ id_vdq :: forall a -> a -> a
+ id_vdq t x = x -- defn site: `a` is visibly bound to `t`
+ call_id_vdq = id_vdq Bool True -- call site: `a` is visibly instantiated to `Bool`
+
+In the equation for ``id`` there is just one binder on the LHS, ``x``, and it
+corresponds to the value argument, not to the type argument. Compare that with
+the definition of ``id_vdq``::
+
+ id_vdq :: forall a -> a -> a
+ id_vdq t x = x
+
+This time we have two binders on the LHS:
+
+* ``t``, corresponding to ``forall a ->`` in the signature
+* ``x``, corresponding to ``a ->`` in the signature
+
+The bound ``t`` can be used in subsequent patterns, as well as on the right-hand
+side of the equation::
+
+ id_vdq :: forall a -> a -> a
+ id_vdq t (x :: t) = x :: t
+ -- ↑ ↑ ↑
+ -- bound used used
+
+We use the terms "visible type argument" and "required type argument"
+interchangeably.
Relation to :extension:`TypeApplications`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -70,12 +122,12 @@ not reflected syntactically in the expression, it is invisible unless we use a
Required type arguments are compulsory. They must appear syntactically at call
sites::
- x1 = id_vdq (type Bool) True -- OK
- x2 = id_vdq True -- not OK
+ x1 = id_vdq Bool True -- OK
+ x2 = id_vdq True -- not OK
You may use an underscore to infer a required type argument::
- x3 = id_vdq (type _) True -- OK
+ x3 = id_vdq _ True -- OK
That is, it is mostly a matter of syntax whether to use ``forall a.`` with type
applications or ``forall a ->``. One advantage of required type arguments is that
@@ -92,20 +144,265 @@ With :extension:`RequiredTypeArguments`, we can imagine a slightly different API
sizeOf :: forall a -> Storable a => Int
-If ``sizeOf`` had this type, we could write ``sizeOf (type Bool)`` without
+If ``sizeOf`` had this type, we could write ``sizeOf Bool`` without
passing a dummy value.
+Required type arguments are erased during compilation. While the source program
+appears to bind and pass required type arguments alongside value arguments, the
+compiled program does not. There is no runtime overhead associated with required
+type arguments relative to the usual, invisible type arguments.
+
Relation to :extension:`ExplicitNamespaces`
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The ``type`` keyword that we used in the examples is not actually part of
-:extension:`RequiredTypeArguments`. It is guarded behind
-:extension:`ExplicitNamespaces`. As described in the proposal, required type
-arguments can be passed without a syntactic marker, making them syntactically
-indistinguishble from ordinary function arguments::
+A required type argument is syntactically indistinguishable from a value
+argument. In a function call ``f arg1 arg2 arg3``, it is impossible to tell,
+without looking at the type of ``f``, which of the three arguments are required
+type arguments, if any.
+
+At the same time, one of the design goals of GHC is to be able to perform name
+resolution (find the binding sites of identifiers) without involving the type
+system. Consider: ::
+
+ data Ty = Int | Double | String deriving Show
+ main = print Int
+
+In this example, there are two constructors named ``Int`` in scope:
+
+* The **type constructor** ``Int`` of kind ``Type`` (imported from ``Prelude``)
+* The **data constructor** ``Int`` of type ``Ty`` (defined locally)
+
+How does the compiler or someone reading the code know that ``print Int`` is
+supposed to refer to the data constructor, not the type constructor? In GHC,
+this is resolved as follows. Each identifier is said to occur either in
+**type syntax** or **term syntax**, depending on the surrounding syntactic
+context::
+
+ -- Examples of X in type syntax
+ type T = X -- RHS of a type synonym
+ data D = MkD X -- field of a data constructor declaration
+ a :: X -- RHS of a type signature
+ b = f (c :: X) -- RHS of a type signature (in expressions)
+ f (x :: X) = x -- RHS of a type signature (in patterns)
+
+ -- Examples of X in term syntax
+ c X = a -- LHS of a function equation
+ c a = X -- RHS of a function equation
+
+One could imagine the entire program "zoned" into type syntax and term syntax,
+each zone having its own rules for name resolution:
+
+* In type syntax, type constructors take precedence over data constructors.
+* In term syntax, data constructors take precedence over type constructors.
+
+This means that in the ``print Int`` example, the data constructor is selected
+solely based on the fact that the ``Int`` occurs in term syntax. This is firmly
+determined before GHC attempts to type-check the expression, so the type of
+``print`` does not influence which of the two ``Int``\s is passed to it.
+
+This may not be the desired behavior in a required type argument. Consider::
+
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
+
+ s1 = vshow Int 42 -- "42"
+ s2 = vshow Double 42 -- "42.0"
+
+The function calls ``vshow Int 42`` and ``vshow Double 42`` are written in
+*term* syntax, while the intended referents of ``Int`` and ``Double`` are the
+respective *type* constructors. As long as there are no data constructors named
+``Int`` or ``Double`` in scope, the example works as intended. However, if such
+clashing constructor names are introduced, they may disrupt name resolution::
+
+ data Ty = Int | Double | String
+
+ vshow :: forall a -> Show a => a -> String
+ vshow t x = show (x :: t)
+
+ s1 = vshow Int 42 -- error: Expected a type, but ‘Int’ has kind ‘Ty’
+ s2 = vshow Double 42 -- error: Expected a type, but ‘Double’ has kind ‘Ty’
+
+In this example the intent was to refer to ``Int`` and ``Double`` as types, but
+the names were resolved in favor of data constructors, resulting in type errors.
+
+The example can be fixed with the help of :extension:`ExplicitNamespaces`, which
+allows embedding type syntax into term syntax using the ``type`` keyword::
+
+ s1 = vshow (type Int) 42
+ s2 = vshow (type Double) 42
+
+A similar problem occurs with list and tuple syntax. In type syntax, ``[a]`` is
+the type of a list, i.e. ``Data.List.List a``. In term syntax, ``[a]`` is a
+singleton list, i.e. ``a : []``. A naive attempt to use the list type as a
+required type argument will result in a type error::
+
+ s3 = vshow [Int] [1,2,3] -- error: Expected a type, but ‘[Int]’ has kind ‘[Type]’
+
+The problem is that GHC assumes ``[Int]`` to stand for ``Int : []`` instead of
+the intended ``Data.List.List Int``. This, too, can be solved using the ``type`` keyword::
+
+ s3 = vshow (type [Int]) [1,2,3]
+
+Since the ``type`` keyword is merely a namespace disambiguation mechanism, it
+need not apply to the entire type argument. Using it to disambiguate only a part
+of the type argument is also valid::
+
+ f :: forall a -> ... -- `f`` is a function that expects a required type argument
+
+ r1 = f (type (Either () Int)) -- `type` applied to the entire type argument
+ r2 = f (Either (type ()) Int) -- `type` applied to one part of it
+ r3 = f (Either (type ()) (type Int)) -- `type` applied to multiple parts
+
+That is, the expression ``Either (type ()) (type Int)`` does *not* indicate that
+``Either`` is applied to two type arguments; rather, the entire expression is a
+single type argument and ``type`` is used to disambiguate parts of it.
+
+Outside a required type argument, it is illegal to use ``type``:
+::
+
+ r4 = type Int -- illegal use of ‘type’
+
+Finally, there are types that require the ``type`` keyword only due to
+limitations of the current implementation::
+
+ a1 = f (type (Int -> Bool)) -- function type
+ a2 = f (type (Read T => T)) -- constrained type
+ a3 = f (type (forall a. a)) -- universally quantified type
+ a4 = f (type (forall a. Read a => String -> a)) -- a combination of the above
+
+This restriction will be relaxed in a future release of GHC.
+
+Effect on implicit quantification
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Implicit quantification is said to occur when GHC inserts an implicit ``forall``
+to bind type variables::
+
+ const :: a -> b -> a -- implicit quantification
+ const :: forall a b. a -> b -> a -- explicit quantification
+
+Normally, implicit quantification is unaffected by term variables in scope:
+::
+ f a = ... -- the LHS binds `a`
+ where const :: a -> b -> a
+ -- implicit quantification over `a` takes place
+ -- despite the `a` bound on the LHS of `f`
+
+When :extension:`RequiredTypeArguments` is in effect, names bound in term syntax
+are not implicitly quantified. This allows us to accept the following example: ::
+
+ readshow :: forall a -> (Read a, Show a) => String -> String
+ readshow t s = show (read s :: t)
+
+ s1 = readshow Int "42" -- "42"
+ s2 = readshow Double "42" -- "42.0"
+
+Note how ``t`` is bound on the LHS of a function equation (term syntax), and
+then used in a type annotation (type syntax). Under the usual rules for implicit
+quantification, the ``t`` would have been implicitly quantified: ::
+
+ -- RequiredTypeArguments
+ readshow t s = show (read s :: t) -- the `t` is captured
+ -- ↑ ↑
+ -- bound used
+
+ -- NoRequiredTypeArguments
+ readshow t s = show (read s :: t) -- the `t` is implicitly quantified as follows:
+ readshow t s = show (read s :: forall t. t)
+ -- ↑ ↑ ↑
+ -- bound bound used
+
+On the one hand, taking the current scope into account allows us to accept
+programs like the one above. On the other hand, some existing programs will no
+longer compile: ::
+
+ a = 42
+ f :: a -> a -- RequiredTypeArguments: the top-level `a` is captured
+
+Because of that, merely enabling :extension:`RequiredTypeArguments` might lead
+to type errors of this form::
+
+ Term variable ‘a’ cannot be used here
+ (term variables cannot be promoted)
+
+There are two possible ways to fix this error::
+
+ a = 42
+ f1 :: b -> b -- (1) use a different variable name
+ f2 :: forall a. a -> a -- (2) use an explicit forall
+
+If you are converting a large codebase to be compatible with
+:extension:`RequiredTypeArguments`, consider using
+:ghc-flag:`-Wterm-variable-capture` during the migration. It is a warning that
+detects instances of implicit quantification incompatible with
+:extension:`RequiredTypeArguments`: ::
+
+ The type variable ‘a’ is implicitly quantified,
+ even though another variable of the same name is in scope:
+ ‘a’ defined at ...
+
+.. _pi-types:
+
+Relation to Π-types
+~~~~~~~~~~~~~~~~~~~
+
+Both ``forall a.`` and ``forall a ->`` are dependent quantifiers in the narrow
+sense defined in :ref:`dependent-quantifier`. However, neither of them
+constitutes a dependent function type (Π-type) that might be familiar to users
+coming from dependently-typed languages or proof assistants.
+
+* Haskell has always had functions whose result *value* depends on
+ the argument *value*::
+
+ not True = False -- argument value: True; result value: False
+ (*2) 5 = 10 -- argument value: 5; result value: 10
+
+ This captures the usual idea of a function, denoted ``a -> b``.
+
+* Haskell also has functions whose result *type* depends on the argument *type*:
+ ::
+
+ id @Int :: Int -> Int -- argument type: Int; result type: Int -> Int
+ id_vdq Bool :: Bool -> Bool -- argument type: Bool; result type: Bool -> Bool
+
+ This captures the idea of parametric polymorphism, denoted ``forall a. b`` or
+ ``forall a -> b``.
+
+* Furthermore, Haskell has functions whose result *value* depends on the
+ argument *type*::
+
+ maxBound @Int8 = 127 -- argument type: Int8; result value: 127
+ maxBound @Int16 = 32767 -- argument type: Int16; result value: 32767
+
+ This captures the idea of ad-hoc (class-based) polymorphism,
+ denoted ``C a => b``.
+
+* However, Haskell does **not** have direct support for functions whose result
+ *type* depends on the argument *value*. In the literature, these are often
+ called "dependent functions", or "Π-types".
+
+ Consider: ::
+
+ type F :: Bool -> Bool
+ type family F b where
+ F True = ...
+ F False = ...
+
+ f :: Bool -> Bool
+ f True = ...
+ f False = ...
+
+ In this example, we define a type family ``F`` to pattern-match on ``b`` at
+ the type level; and a function ``f`` to pattern-match on ``b`` at the term
+ level. However, it is impossible to quantify over ``b`` in such a way that
+ both ``F`` and ``f`` could be applied to it::
+
+ depfun :: forall (b :: Bool) -> F b -- Allowed
+ depfun b = ... (f b) ... -- Not allowed
- n = id_vdq Integer 42
+ It is illegal to pass ``b`` to ``f`` because ``b`` does not exist at runtime.
+ Types and type arguments are erased before runtime.
-In this example we pass ``Integer`` as opposed to ``(type Integer)``.
-This means that :extension:`RequiredTypeArguments` is not tied to the ``type``
-syntax, which belongs to :extension:`ExplicitNamespaces`.
\ No newline at end of file
+The :extension:`RequiredTypeArguments` extension does not add dependent
+functions, which would be a much bigger step. Rather :extension:`RequiredTypeArguments`
+just makes it possible for the type arguments of a function to be compulsory.
\ No newline at end of file
=====================================
docs/users_guide/using-warnings.rst
=====================================
@@ -2440,8 +2440,8 @@ of ``-W(no-)*``.
For example: ::
a = 15
- f :: a -> a -- Does ‘a’ refer to the term-level binding
- -- or is it implicitly quantified?
+ f :: a -> a -- NoRequiredTypeArguments: The ‘a’ is implicitly quantified
+ -- RequiredTypeArguments: The ‘a’ refers to the term-level binding
When :ghc-flag:`-Wterm-variable-capture` is enabled, GHC warns against implicit quantification
that would stop working under :extension:`RequiredTypeArguments`.
=====================================
m4/xcode_version.m4 deleted
=====================================
@@ -1,25 +0,0 @@
-# XCODE_VERSION()
-# --------------------------------
-# Gets the version number of Xcode, if on a Mac
-AC_DEFUN([XCODE_VERSION],[
- if test "$TargetVendor_CPP" = "apple"
- then
- AC_MSG_CHECKING(Xcode version)
- XcodeVersion=`(xcode-select -p > /dev/null 2>&1 && xcodebuild -version) | grep Xcode | sed "s/Xcode //"`
- # Old Xcode versions don't actually give the Xcode version
- if test "$XcodeVersion" = ""
- then
- AC_MSG_RESULT(not found (too old?))
- XcodeVersion1=0
- XcodeVersion2=0
- else
- AC_MSG_RESULT($XcodeVersion)
- XcodeVersion1=`echo "$XcodeVersion" | sed 's/\..*//'`
- changequote(, )dnl
- XcodeVersion2=`echo "$XcodeVersion" | sed 's/[^.]*\.\([^.]*\).*/\1/'`
- changequote([, ])dnl
- AC_MSG_NOTICE(Xcode version component 1: $XcodeVersion1)
- AC_MSG_NOTICE(Xcode version component 2: $XcodeVersion2)
- fi
- fi
-])
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3ed7a7e9556d12c18d870f1f6574edb4eb9fab0e...c9e17a97351fe824109cabdce67986b3fe0065f9
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/compare/3ed7a7e9556d12c18d870f1f6574edb4eb9fab0e...c9e17a97351fe824109cabdce67986b3fe0065f9
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20231212/89323cf7/attachment-0001.html>
More information about the ghc-commits
mailing list