New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Visible forall
in types of terms, and types in terms
#281
Conversation
Seeing as, apparently, the only difference between And some bikeshedding - while, in principle, I prefer the capitalization of |
Sounds reasonable, but this would be a breaking change. Consider:
Which |
The proposal says:
One way to meet "require an explicit type argument" is to write applications as It's worth noting that, as proposed,
I am open to that as a future possiblity but, as you know, I am not ready to commit to it. I'd like to accept or reject this propsoal on its own merits. |
I added this as an alternative and explained why I don't think it's a good one.
To be clear, reinterpretation as proposed does not change how the names were resolved. That is, if
This proposal is a step towards a destination, and if we disagree about the destination, I'm not sure we should invest time and effort into making this step. That is, I don't believe this proposal has a good power-to-weight ratio if we look at it in isolation. Looking at the motivation section, we have:
But: Point 3 refers to pi-types, which will require term/type unification either way. Point 1 is about symmetry between terms and types, which means little if we do not seek to unify them. Point 2 alone is not sufficient to make this proposal worthwhile (in my opinion). |
I just want to be careful about language here. It is sad that the renaming of a visible dependent argument is different than that of a specified dependent argument. Maybe it is inevitable, but it's sad. If we imagine dependent Haskell, it will be a wart on the language. If we end up accepting this proposal as currently written, I would welcome a separate proposal (or maybe a rider on this one) that we add a warning to
This doesn't seem right. Consider an argument Do we need to make Maybe it's s good idea to make
This section is almost worthy of its own proposal. With my GHC-committee hat on (leaving my Dependent-Types hat to the side), I'm very dubious of this. And I don't see it as essential here. I understand that the proposal process is onerous, and I'm sympathetic to attempts to short-circuit it. Indeed, I support the suggestion you have here (as long as the changes are non-breaking -- fixing Nice example. I do not see a need for a new extension here. We have too many extensions! Just hook into We don't have a unified type/term parser yet, do we? This proposal is designed assuming that these parsers are mergeable. That may be true, but I don't yet have evidence of it. Is this simply impossible because of On the other hand, it would seem a waste of effort to merge these parsers without the acceptance of this proposal, unless it served to reduce complexity in the parser and improve error messages. I'm unsurprisingly in favor, in general. |
It is worth noting that making |
Yes, "
This is resolved by #270, no? With
Right, I removed the part about fixities.
Assume we do not make Before we get to type-checking (where reinterpretation should happen), we do name resolution. We end up trying to resolve The real question is not whether to make
Not to say that it's impossible, but it would require some fancy footwork. Every discrepancy between terms and types is a burden.
I added "non-breaking" to clarify the intent.
The thought process behind this is that by introducing this reinterpretation business, we add a bit of ugly complexity, but at least we plan to get rid of it down the line. If we don't agree that we should be moving away from reinterpretation of terms as types, and towards unification of terms with types, then maybe we shouldn't be adding reinterpretation in the first place. It's scaffolding, not the final product. |
I disagree, but not strongly. Added to alternatives, happy to do whatever the committee decides about this.
I'm happy to do go ahead and merge them, but before I do this, let's agree first that this is even a thing we want to do!
Sure, then we'll do either of these things:
I only expect that we first agree that this is the direction we all want to go in, and so far @simonpj indicated that this is not necessarily the case. |
The search query doesn't seem right to me, as the results include identifiers such as |
No. Do not use the first person there. I think you mean the elite and increasingly exclusive brethren at GHC HQ want to unify terms/types. Fine. Suggest you stop calling the resulting language 'Haskell'. |
I'll point out that both Simon and I have balked at the bit of the proposal you're criticizing here. I personally do think this is a good direction of travel, but I wouldn't presume to say that others do, too.
I'll point out that name lookup failures do not stop the compilation pipeline. They don't even induce warnings or errors! (It's trying to give them a type that produces the errors.) So I still claim that this is possible. Maybe not preferable, but possible.
Not quite. While |
Thank you Richard, I apologise my intemperate language was a (visceral) reaction against @int-index's high-handed presumption. If there's some merit to unifying types/terms, Vladislav needs to carry everybody with him by persuading and demonstrating how it supports better programming (for some value of 'better'). We've always had unified syntax for type construction and data construction; and somewhat similar for pattern matching (if we allow class and TF instances as type-level patterns). That doesn't persuade me we have or need unified semantics; because ... GHC Haskell (even more than Hugs Haskell) is a multi-module compiled language. There's a phase distinction between the semantics at compile time (type inference) vs execution time. Needing to support multi-module (where the compiler can't know what other modules this might get imported into) puts a hard block on what can happen when. I think it's important users of Haskell understand that distinction. Even if the language tries to unify types/terms, that distinction will 'grin through' the abstraction. |
To @AntC2,
In this particular sentence, "we" refers to everyone involved in the discussion. I see that you disagree – alright, then it's up to me to improve the Motivation section until that phrase, "we all agree that the term/type unification is The Right Thing", becomes true. Note how it is prefixed by "by accepting this proposal". Let's not accept it until we reach consensus.
I'm afraid this argument went over my head. There are other multi-module compiled languages, which are dependently typed and use the same language for types and terms. Could you demonstrate how this distinction grins through the abstraction in those languages, using the one most familiar to you? (I'll make the effort to understand the example whatever language you pick, but I'm most familiar with Agda/Coq/Idris) To @goldfirere,
That's something I didn't realize. I think there are other ways this hack may fail. For example:
This results in an error before the type checker:
In general, I'm very wary of reinterpreting syntactic constructs. Parsing So, why would we add new faulty code like this, while firefighting its consequences in other places? The reason reinterpretation as described in this proposal isn't that bad is that there are direct equivalences between the reinterpreted constructs:
... and so on. The reinterpretation of terms as types is direct. My hope is that in the end, we can fully unify them, removing the need even for a direct reinterpretation. On the other hand, parsing
What if |
There you go again making a high-handed presumption (in fact much the same presumption) that Haskell must become a dependently-typed language. It's a lot less than clear how we get there from a language whose typing theory was originally based on Damas-Hindley-Milner. It's an open research question whether such a migration is possible without breaking too much. My guess is it's hard; and that you might end up with a language that is 'based on Haskell' but is not Haskell. You need to not only improve the Motivation section here, but the Motivation for each step along the journey. There's currently no roadmap. Section 4 Meta is not a roadmap, it reads more like handing over the hen-house to the fox. (This is my favourite language you're messing with. Already the fluffy chicks I first knew have become cantankerous broilers.)
It's already grinning through in a small way. With promoted
(And of course real-life terms will be more complex) I'm seeing To understand the semantics I need to bear in mind: terms are evaluated left-to-right by Beta-reduction; types are solved Outside-In by unification. (Yes that's a gross simplification.)
Those languages designed from the ground up for Dependent Typing: do they support punning type-names as term-level names; and punning term-level literals as types?
Coq is a theorem-prover not comparable to Haskell; Agda/Idris are as much theorem-provers/proof assistants as programming languages. I don't see any of them as achieving the industrial-strength optimised object code that Haskell achieves. And thank you for the invitation, but no I'm not going to enter into some language war. As @simonpj already said "I'd like to accept or reject this propsoal on its own merits." The argument you're making implicitly 'This proposal moves Haskell closer to Coq/Agda/Idris' does not give any merits. |
(@int-index you might want to edit the PR name and description to "in types of terms" as well?) |
I want to add that point 2 is enough for me to consider this proposal useful and worthy to be implemented. It opens a possibility to improve the UX of Haskell users which I value a lot (and I think we all should care about improving Haskell UX for beginners, but that's just my opinion). Haskell has a reputation for being non-beginner-friendly and with this feature, developers can implement better libraries. Below I'm going to provide a few examples from production usage of Haskell where I can find this feature useful.
As you can see from my examples, I often want to be able to force users to specify the type of argument explicitly. It's often useful that with |
I think this is good enough. I am fine with people using multiple namespaces thinking of |
As to the eventual goals discussion, I think it's important to remember that these are ghc-proposals not haskell-proposals. I am fine rebranding "Dependent Haskell" as, I dunno, "Alonzo", if we agree that GHC should support both and they should freely interoperate type safely. Now, when this proposal says
We should understand not as
but as:
I think that's hard to argue against. The people working on GHC which to research these things. This proposal is inarguably a good step in service of that goal. Haskell 98 remains Haskell 98. What's the problem? |
Yes where I'm coming from is the UX. For beginners we used to offer an easier experience, with the mind-twisting bits hidden away behind extensions. Then I'm very puzzled by @chshersh's comment. Haskell 98, and even including common extensions such as MPTCs is user friendly. What has made GHC Haskell non-beginner-friendly is that it's increasingly difficult to hide the mind-twisting bits. I see this proposal as one more twist.
Well yes maybe (for some value of 'better'). The examples you give of better libraries: do you expect beginners to use them, with explicit type application? And without some syntactic marking that types are appearing in terms? That seems to me the opposite of beginner-friendly. To remind, the story we give to beginners is:
Unfortunately GHC is currently failing at point 1. If you write a dodgy signature (which beginners are very prone to), GHC rather than saying that's probably not what you meant, recommends you switch on
I have no view on that. Remember GHC's core is not Haskell, and has always had explicit type application; that's compulsory explicit-type-application-everywhere. Remember that GHC core is type-checked; but has no type improvement/type inference mechanisms. That's OK as an intermediate language whose type applications are generated mechanically. Nobody writes core by hand do they? That would be like bit-aligning and byte/word-aligning data layouts by hand. For some features from core, it has been useful to expose them in surface Haskell. Compulsory explicit-type-application-everywhere is not one of those features. I (for one) don't expect beginners to look at core; I don't expect they'll know that core has explicit type application; I do position Haskell for beginners as a High Level Language which to a large extent looks after the types for itself. If you enjoy burdening your code with type-management, C is a fine language. |
@AntC2 With all due respect, please knock it off. Virtually nothing you've written on this thread pertains to this specific proposal. It's all general grousing about the direction of GHC. Let's be clear: I've been to many talks by Richard and others on the work being done to bring dependent types to haskell. Invariably, the first question, to significant applause, is "how soon can we get it?" So yes, there is great demand for this, and there are many proposals pertaining to it. If you don't like that direction -- go find a better venue to convince people otherwise. Write to a mailing list, write a blog post. Complain on reddit. But derailing specific proposals over your complaints about a general direction that many people, with much support, are working towards -- that's not appropriate, and I wish you would stop. |
To @glaebhoerl,
Yes, thank you. Fixed it. To @chshersh, Thank you for all the examples. I'm not sure what would be a good way to incorporate them into the proposal, as it is a matter of judgement whether to use visible or invisible But it's still valuable to see these examples in the discussion, and to know that visible To @AntC2,
I'm rather of the opinion that Haskell should provide an option of dependent typing, as I find it immensely useful, but it's up to the programmer whether to make use of dependent types.
The proposed change is hidden behind an extension,
Let's put dependent types aside for the moment. As far as I understand your arguments, you care a lot about making Haskell beginner-friendly (so do I). But then, the consistent thing would be to become a proponent of term/type unification and getting rid of punning. In my teaching experience, it's difficult for beginners to keep track of the current context, and to realize that So, even without dependent types, using a single language for terms and types, and eschewing punning, would be a win.
With all the extensions that were added to GHC, the inference is not any worse as long as you do not enable them. So I don't think that GHC is failing here, its inference engine is a blazing success.
I'm afraid there are differences between C and Haskell other than the amount of required type annotations.
This was not an invitation for a language war, but an attempt to understand your point of view on the matter. As far as I can tell, the argument goes like this:
I don't believe we can jump from (2) to (3), and the existence of other multi-module compiled languages with dependent types is evidence that I used to back up the claim that, in fact, term/type unification is a very reasonable thing to have in a multi-module compiled language such as Haskell. But of course I'm always considering the possibility that I'm wrong, so I asked you to compromise my evidence, so that I could change my view and we'd end up on the same page. The goal of this argument is to arrive at the consensus, is it not? Just to reiterate, I think the following holds true:
Or, as @Ericson2314 puts it:
Finally, to @gbaz,
I appreciate the fervor of your comment, but I think this venue is perfectly fine. We are discussing an addition to Haskell, and, furthermore, a new policy about future additions! I like to believe that @AntC2 argues in good faith, trying to do the best for Haskell. Except we don't quite agree on what would be best. It is true that Haskell 2010 is a different spot in the design space than Dependent Haskell. It has name punning, it has better inference at the expense of other features. @AntC2 enjoys this spot in the design space and tries to protect it from the invasive changes, motivated by dependent types, that threaten it. And it's a noble thing to do that. I like Haskell 2010 as well. But! I don't believe we are threatening it. The reason Dependent Haskell isn't a new language but an extension of Haskell is that it's designed to have perfect interoperability with Haskell 2010. GHC will continue to implement Haskell 2010, and the new features are to be hidden behind extension flags as appropriate. I would much prefer that @AntC2 and the dependent types crowd (of which I'm a vocal member) would realize that we don't need to be at odds with each other. And we should not exclude anyone from the conversation. |
Regarding the proposal as it stands (rather than as a pathway to something more ambitious), this ability to specify a compulsory type argument looks like the main benefit. And I agree that it is a benefit, and it's one that is quite independent of the full-spectrum dependency issue. The question is: how much does this benefit cost. The main cost is resolving the syntactic and name-space difference between types and terms. On obvious way of resolving that is via a syntactic marker. We already have one, namely @. So we could use @ for those compulsory type arguments too. This would be simple to explain, and require none of this re-interpretation. But it would occasionally be inconvenient. For example, if |
@simonpj I added this as another alternative. Unsurprisingly, I'm not enamored with it either, as the primary motivation for me is to blur the distinction between terms and types, not to make it stand out with a syntactic marker. |
@int-index I would to add to that alternative that even without of dependent types we may want want invisible relevant non-dependent quantification (that is to say, |
I hate to be negative, but I personally would rather do away with this proposal than to require the |
OK. Would you like to say why it seems like a step in the wrong direction? |
It moves us away from uniformity. Let's even pretend for a moment that I'm not trying to actually merge the term-level and type-level. Right now, we can say this: type VDQ :: forall k1. forall k2 -> k1 -> k2 -> Type
data VDQ k2 a b
type VDQIntTrue = VDQ @Type Bool Int True
type VDQCharFalse = VDQ Bool Char False If we were to require the vid :: forall a. forall b -> a -> b -> ()
vid _ _ _ = ()
ex1 = vid @Int @Bool 3 True
ex2 = vid @_ @Bool 'x' False These look different! Why different syntaxes for the same idea? Worse, imagine a data constructor: data Silly a b where
Mk :: forall a. forall b -> a -> b -> Silly a b Now we have this oddity: type Different1 = Mk @Nat Bool 3 True
type Different2 = Mk Bool "hi" False
different3 = Mk @Int @Bool 3 True
different4 = Mk @_ @Bool "hi" False Here, the right-hand sides should be the same, but they have to be different. Today, we have non-uniformity by omission: we have no visible |
If I wanted to define a type Storable :: Type -> Constraint
class Storable a where
sizeOf :: Int The default type of sizeOf :: forall a. Storable a => Int but if I wanted a visible quantifier, is my only hope to define a new function? sizeOf :: forall a -> Storable a => Int |
Yes. But improvements have been wondered about. See #236, for example. |
While not strictly necessary for the proposal, I think it would be valuable to point out that the nicerReify :: forall a r. a -> (forall (s :: *) -> Reifies s a => r) -> r |
forall
in types of terms, and types in terms
The proposal contradicts itself (elsewhere it says "Any uses of terms in types are ill-typed") and treating term variables as skolems can be handled in a later proposal
@int-index I have a question about how this interacts with #448. After presenting the new the syntax rule to allow
In #23704 you say "GHC Proposals #281 and #402 allow the use of visible forall in data constructors.". Does/should this proposal allow types (rather than just variables and wildcards) in constructor patterns for visible Update: I just saw that the proposal states
so I retract my question, sorry for the noise |
@JakobBruenker Actually, I want to answer that question. Yes, we need a pattern-to-type-pattern mapping, the issue for it is #23739. We need it even if we don't relax the restriction you cited because it will affect error messages. Furthermore, I believe the restriction was added only because we didn't know how to handle higher-kinded variables (#18986). We figured it out, so the restriction can be lifted. In fact, I now believe it must be lifted because it creates a bad inconsistency. Let's say we have data TInvis a where
TypedInvis :: forall a. a -> TInvis a
g :: TInvis Int -> ...
g (TypedInvis @Int x) = ... The restriction means that I can't change |
That makes sense! Thanks for the explanation |
@int-index I have one more question: The proposal contains the typing rule: G |- sigma[a := rho]; pis ~> Theta; phis; rho_r
------------------------------------------------------------------ ITVDQ
G |- (forall a -> sigma); (type rho), pis ~> Theta; phis; rho_r It requires that the argument that's passed is a ghci> id @(forall a . a) undefined
*** Exception: Prelude.undefined What is the reason for not allowing them for required type arguments? I have a version of GHC HEAD from July which also allows ghci> id' :: forall a -> a -> a; id' (type _) = id
ghci> id' (type (forall a . a)) undefined
*** Exception: Prelude.undefined This seems to suggest that the implementation does allow any σ-type? |
@JakobBruenker Good question. I don't quite remember why I used |
easy to fix, as part of #626 |
**Description** The Copilot API offers the function `Copilot.Language.Spec.forall`, which future versions of GHC will disallow. To ensure that Copilot keeps working with future versions of the compiler, this function should be renamed. **Type** - Management: change to keep Copilot working with future versions of the language/compiler. **Additional context** The proposal was filed in ghc-proposals/ghc-proposals#281, and subsequently accepted in GHC. Details are also available at: https://downloads.haskell.org/ghc/latest/docs/users_guide/using-warnings.html#ghc-flag--Wforall-identifier. **Requester** - Ivan Perez **Method to check presence of bug** Although not a bug, it is possible to detect the presence of this issue by compiling with GHC >= 9.4. Using `-Werror=forall-identifier` will make the issue become a compile-time error. We cannot yet use a test that will produce a failure (expected) if forall is defined (i.e., with -Werror=forall-keyword) because we have to deprecate the function before we remove it. The following Dockerfile checks that the function forall has been deprecated and that the alterative forAll is offered, in which case prints the message Success: ``` FROM ubuntu:focal RUN apt-get update RUN apt-get install --yes libz-dev RUN apt-get install --yes git RUN apt-get install --yes wget RUN mkdir -p $HOME/.ghcup/bin RUN wget https://downloads.haskell.org/~ghcup/0.1.19.2/x86_64-linux-ghcup-0.1.19.2 -O $HOME/.ghcup/bin/ghcup RUN chmod a+x $HOME/.ghcup/bin/ghcup ENV PATH=$PATH:/root/.ghcup/bin/ ENV PATH=$PATH:/root/.cabal/bin/ RUN apt-get install --yes curl RUN apt-get install --yes gcc g++ make libgmp3-dev SHELL ["/bin/bash", "-c"] RUN ghcup install ghc 9.4 RUN ghcup install cabal 3.2 RUN ghcup set ghc 9.4.8 RUN cabal update SHELL ["/bin/bash", "-c"] CMD git clone $REPO && cd $NAME && git checkout $COMMIT && cd .. \ && cabal v1-sandbox init \ && cabal v1-install alex happy \ && cabal v1-install copilot/**/ \ && ! cabal v1-exec -- runhaskell -Werror=deprecations <<< 'import Copilot.Language (true, forall, theorem); spec = theorem "true" (forall true); main :: IO (); main = pure ();' \ && cabal v1-exec -- runhaskell -Werror=forall-identifier -Werror=deprecations <<< 'import Copilot.Language (true, forAll, theorem); spec = theorem "true" (forAll true); main :: IO (); main = pure ();' \ && echo "Success" ``` Command (substitute variables based on new path after merge): ``` $ docker run -e "REPO=https://github.com/Copilot-Language/copilot" -e "NAME=copilot" -e "COMMIT=<HASH>" -it copilot-verify-470 ``` **Expected result** Running the Dockerfile above prints the message "Success", indicating that the old forall function is deprecated and a new variant is being offered. **Solution implemented** Introduce a new function `forAll` that implements the behavior currently implemented by `forall`. Replace all references of `forall` to point to `forAll`, including occurrences in tests and examples. Deprecate `forall`. **Further notes** None.
The proposal has been accepted; the following discussion is mostly of historic interest.
We propose to allow visible irrelevant dependent quantification, written as
forall x ->
, in types of terms.Rendered