Skip to content
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

Add support for top-level declaration and module annotations #4482

Open
JordanMartinez opened this issue Jul 6, 2023 · 21 comments
Open

Add support for top-level declaration and module annotations #4482

JordanMartinez opened this issue Jul 6, 2023 · 21 comments

Comments

@JordanMartinez
Copy link
Contributor

JordanMartinez commented Jul 6, 2023

Summary

Add support for annotations on top-level declarations and modules.

Motivation

Marking a module or top-level declaration with additional information unrelated to its type or kind signature would be useful for some purpose (e.g. codegen, documentation, etc.). However, the current language does not support a way to add such an annotation to such declarations or modules. Examples of where this would be useful include:

  • diagnostics:
    • Deprecation - While the Warn type class can be used to indicate deprecation on values/functions, it cannot be used on types or data constructors.
    • Linting. allow, warn, deny, forbid - these can be useful to fail the build if an undesirable code pattern is used (e.g. avoiding a known code pattern that arises due to React not using referential transparency).
    • a warning suppressor attribute - I can see this being useful for one-off hiding of some compiler warnings but not all of that particular type
  • Codegen purposes.
    • I wrote purescript-tidy-codegen-lens to automatically generate optics for a given type. While we don't support something like TemplateHaskell, annotating a type is something that could be used by the IDE to generate optics for that type using this program.
    • Similarly, one could codegen a value-based JSON codec for a type using similar means, removing one of the main reasons (i.e. convenience) why many use typeclass-based JSON codecs rather than value-based ones. However, this argument is weakened if Support deriving via #3302 were implemented.
  • Inline directives.
    • As discussed and then blocked (?) in Allow outputting declaration-level comments in CoreFn #4442, it would be ideal if inline directives consumed by the backend-optimizer project could be encoded as annotations. This would enable the directive to be declared near its declaration site rather than in the module comment.
  • Output modifications.
    • For the JS backend, indicating via a module-level annotation which identifier (or a record containing identifiers) should be exported as export default. See this comment for details.
  • Testing:
    • indicating which functions are tests - I can see this being useful as a replacement for purescript-spec-discovery, which didn't work when I last tried it.
  • FFI/linking:
    • link - Rust summarizes this as, "Specifies a native library to link with an extern block." I imagine something similar would be the case for non-JS backends. For JS backends, this could potentially be used to indicate to spago which NPM dependencies to install.

I will update this list with more examples as they arise.

Design Questions

I am proposing this feature because my previous attempt at something similar in #4442 was seemingly blocked on the reasoning that we should implement a "real" annotation feature rather than misuse comments for a similar purpose. In the event that this issue produces bikeshedding and comes to a halt, I suppose that will give more reason to continue implementing #4442.

Regardless, being unfamiliar with the core questions an annotation feature's design requires, I thought I would first open this issue and continue it by asking what design questions need to be addressed. I imagine it's something like the following:

  1. What will the syntax be for annotations? I'm assuming we would support some kind of structured data (e.g. arrays/records are supported).
  2. On what entities can annotations be added. I assume modules and most top-level declarations (i.e. value declarations, data declarations, data constructors, type synonym declarations, class declarations, instance declarations, extern declarations, and extern data declarations). I also assume that non-top-level declarations (e.g. let or where bindings) are excluded. I also assume other top-level declarations are excluded (e.g. fixity declarations, role declarations, and kind signatures).
  3. Are there some annotations that have special compiler support that others do not (e.g. a Deprecated annotation causes the compiler to emit a warning)?
  4. How do annotations propagate through CoreFn transformations, and which CoreFn node holds that annotation?
  5. How do top-level mutually recursive binding groups affect the design?
  6. Are there certain conventions (e.g. naming, how annotations are structured, etc.) we want to assume but not enforce? Or others that we enforce?
  7. What other languages do we want to follow or avoid in how they designed their annotation feature?
@f-f
Copy link
Member

f-f commented Jul 7, 2023

This all sounds like we wish to add metadata to different parts of the AST. The examples are varied, but the common point is that this metadata is not for the compiler itself, but only passed through and consumed by humans or tools downstream of the compiler.
Since tools need to work with it, it needs to be unambiguously structured, which I understand is the main objection to just sticking all this stuff in comments in #4442 (and I personally concur with this)

The collection of use-cases that we have in this issue is good, but I think that to go from there to adding a language feature we'd need to see more in detail what kind of information needs to be carried around. The previous proposal used comments, and there's overlap with the proposed deriving via feature - things might get clearer if we do the exercise of trying to cover these usecases with the currently proposed mechanisms. (I also think we should implement deriving via though)

I guess the bottom line is that the bar for adding a language feature at this point is somewhat high since we don't really want to be breaking things all the time if requirements change, and "something to pass metadata through" feels way too underspecified to be warmly welcome without being afraid to break it over time.

It might also be that we don't need a new language feature at all for just passing metadata through. E.g. I don't see how we couldn't cover all the proposed usecases with a very generic Prim.meta :: forall a b. a -> b -> b?

@JordanMartinez
Copy link
Contributor Author

JordanMartinez commented Jul 7, 2023

The examples are varied, but the common point is that this metadata is not for the compiler itself, but only passed through and consumed by humans or tools downstream of the compiler.

Not quite. The deprecation annotation would cause the compiler to emit a warning. So, the compiler is a consumer in some cases.

I guess the bottom line is that the bar for adding a language feature at this point is somewhat high since we don't really want to be breaking things all the time if requirements change, and "something to pass metadata through" feels way too underspecified to be warmly welcome without being afraid to break it over time.

I understand the reasoning here, but we typically break things about once every year. And without actually shipping a feature, it's harder to get feedback about what changes to the design are needed.

I don't see how we couldn't cover all the proposed usecases with a very generic ``Prim.meta :: forall a b. a -> b -> b`?

I find this idea problematic for a few reasons:

  1. This wouldn't allow one to deprecate types or data constructors. At least, it's not clear to me how one would do that.
  2. since it's a curried function, one could apply the annotation as the first arg without applying the second arg (e.g. foo (meta "some annotation")). I think that defeats the purpose of this idea
  3. depending on how large that annotation is, it can clutter actual code with metadata.

@garyb
Copy link
Member

garyb commented Jul 7, 2023

  1. What will the syntax be for annotations? I'm assuming we would support some kind of structured data (e.g. arrays/records are supported).

That sounds good to me, I'd suggest any of the Prim types can be used in the value for an annotation. I'd suggest they also should have sort of label/name component, so there's an easy way for tools that consume annotations to decide how/whether to process them.

Whatever syntax we use, it'd be nice if we could avoid introducing anything new that tramples on the existing namespace. Since we're sticking to top-level things for annotations, I'd suggest that means starting them with a symbol, since symbols are not allowed there otherwise currently, so there's no conflict.

  1. On what entities can annotations be added. I assume modules and most top-level declarations (i.e. value declarations, data declarations, data constructors, type synonym declarations, class declarations, instance declarations, extern declarations, and extern data declarations). I also assume that non-top-level declarations (e.g. let or where bindings) are excluded. I also assume other top-level declarations are excluded (e.g. fixity declarations, role declarations, and kind signatures).

I agree with top level only, as mentioned in my bit about 1. I think the list of things you suggest here covers it!

  1. Are there some annotations that have special compiler support that others do not (e.g. a Deprecated annotation causes the compiler to emit a warning)?

Sure, I can't really think of anything other than a deprecation annotation just now... maybe something about backend targets? It's only sort-of the compiler there though, as it depends on --codegen. (Like, throw an error if we try to compile a module as JS that is annotated as purerl only).

  1. How do annotations propagate through CoreFn transformations, and which CoreFn node holds that annotation?

I don't have any to say about this just now it's a while since I was in there.

  1. How do top-level mutually recursive binding groups affect the design?

I don't think they necessarily need to, aside from whatever is necessary in terms of CoreFn / where the annotation lives in the AST.

  1. Are there certain conventions (e.g. naming, how annotations are structured, etc.) we want to assume but not enforce? Or others that we enforce?

I'd say aside from them having a label and (maybe optional?) associated value that's all the structure they'd need. There's discussion to be had about lexical rules for the label though I guess. Given my suggestions about using a symbol I'm thinking we'd end up with something like:

-- label-only annotation
@Deprecated
someValue :: ...
-- label-with-value annotation
@Target "purerl"
module MyErlangModule where ...
  1. What other languages do we want to follow or avoid in how they designed their annotation feature?

I have no strong feelings about this, C# is the main language I can think of that I interacted with them. They were inoffensive.

@natefaubion
Copy link
Contributor

natefaubion commented Jul 7, 2023

I think that we would want to support annotations on typeclass/instance members, which are not top-level. I could also see annotations on expressions/identifiers, but I recognize that this is a much larger space to look at. It can sometimes be subsumed by value level identity functions, but it assumes:

  • Identity functions are a good way to annotate things (debatable, I think it's strictly worse than using comments).
  • The compiler is not going to have a pre-codegen CoreFn optimization that removes trivial identities.
  • If it will do that, the compiler might need to support an annotation to prevent that.
  • If it won't provide that, the author may need to unnecessarily FFI a binding, which affects all backends, which makes it unlikely for authors to utilize the annotation.

@JordanMartinez
Copy link
Contributor Author

I think that we would want to support annotations on typeclass/instance members, which are not top-level.

Ah... good point. That would be useful for inline directives, right?

@JordanMartinez
Copy link
Contributor Author

Given my suggestions about using a symbol I'm thinking we'd end up with something like:

Would each annotation exist as its own declaration (e.g. 1 per line)? Or would they be grouped under a single declaration (e.g. many per line)?
For example

@Annotation1
@Annotation2
@Annotation3
foo :: String -> ...
foo = ...

or

@[Annotation1, Annotation2, Annotation3]
foo :: String -> ...
foo = ...

-- if things got too long, then it can still be formatted over multiple times
@[ Annotation1
 , Annotation2
 , Annotation3
 ]
foo :: String -> ...
foo = ...

@garyb
Copy link
Member

garyb commented Jul 8, 2023

I think that we would want to support annotations on typeclass/instance members, which are not top-level.

👍

Would each annotation exist as its own declaration (e.g. 1 per line)? Or would they be grouped under a single declaration (e.g. many per line)?

If there's no difference then I'd maybe slightly prefer not having them grouped, but I don't feel particularly strongly about it - if it's easier to parse one over the other, then that one? 😄

@JordanMartinez
Copy link
Contributor Author

I could also see annotations on expressions/identifiers

I could see that as well. But for the time being, could that be considered outside the scope of this? Or put differently, could you provide an example where adding such an annotation would be helpful?

@JordanMartinez
Copy link
Contributor Author

I thought of another use case for annotations, this time at the module-level. ES modules have default exports. What if there was an annotation that indicated (at least for JS backends) which value to export as default in the final codegen?

Given this..

@JsDefault=foo
module Foo where

foo :: String
foo = "bar"

baz :: Int
baz = 1

The outputted JS would be:

export const foo = "bar"
export const baz = 1
export default foo;

I could also imagine something like

@JsDefault={foo, bar}

which would output

export default { foo, bar }

@natefaubion
Copy link
Contributor

Or put differently, could you provide an example where adding such an annotation would be helpful?

My use case was call-site inlining annotations. Additionally, inlining annotations on local bindings could be useful. To me there isn't a distinction between "top-level" and "any declaration context".

@JordanMartinez
Copy link
Contributor Author

Or put differently, could you provide an example where adding such an annotation would be helpful?

My use case was call-site inlining annotations. Additionally, inlining annotations on local bindings could be useful. To me there isn't a distinction between "top-level" and "any declaration context".

My main reason for not supporting that initially was to make this easier to implement and to deal with less edge cases. But, that presumption was mainly due to not knowing how much complexity supporting non-top-level declarations would be. That being said, I agree that this would be useful to have. Do you think it should be included in the initial implementation as opposed to being added later? I'm assuming yes.

@JordanMartinez
Copy link
Contributor Author

What other languages do we want to follow or avoid in how they designed their annotation feature?

Taking a cursory glance at this using Rust. Rust's annotations are called attributes. Some key highlights:

  • Syntax is inspired by C#:
    • Attributes are modeled on Attributes in ECMA-335, with the syntax coming from ECMA-334 (C#).

  • Example of syntax: #[attribute = value], #[attribute(someValue("bar"), another)
  • Outer attributes (i.e. #[foo]) apply to the thing that follows attribute; inner attributes (i.e. #![foo]) apply to the thing in which attribute is declared
  • Some attributes are removed during attribute processing ("active" attributes) while others stay on ("inert" attributes)
  • 3-4 types of attributes:
    • Built-ins
    • Macros & derive macro helper attributes, which is currently irrelevant due to PureScript not having macros
    • Tool attributes, which must exist in the Tool prelude namespace

Looking at some of the use cases they list for attributes, I'll update the opening thread with these as ideas:

  • testing:
    • indicating which functions are tests - I can see this being useful as a replacement for purescript-spec-discovery, which didn't work when I last tried it.
  • linting:
    • a warning suppressor attribute - I can see this being useful for one-off hiding of some compiler warnings but not all of that particular type
  • diagnostics:
    • deprecation
    • allow, warn, deny, forbid - these can be useful to fail the build if an undesirable code pattern is used (e.g. avoiding a known code pattern that arises due to React not using referential transparency).
  • FFI/linking:
    • link - Rust summarizes this as, "Specifies a native library to link with an extern block." I imagine something similar would be the case for non-JS backends. For JS backends, this could potentially be used to indicate to spago which NPM dependencies to install.

@rhendric
Copy link
Member

rhendric commented Jul 20, 2023

I'd like to toss out a design sketch at this point.

Syntax

  • An annotation group is parsed as '{' '{' sep1(expr4, ',') '}' '}', where each expr4 is an independent annotation.
  • Zero or more consecutive annotation groups are valid in the following locations in the grammar:
    • Preceding a module declaration, on its own line
    • Preceding any module-level declaration (including imports, fixity, etc.), on its own line
    • Preceding a let- (or where-) level declaration, on its own line
    • Preceding a class member, on its own line
    • Preceding an instance binding, on its own line
    • Preceding an expr7 (atomic expressions, delimited expressions, and dotted chains), inline
    • Preceding a typeAtom, inline (includes data constructor fields)
    • Preceding a data constructor definition, inline
    • (more?)

Examples:

{{Deprecated "use other thing instead"}}
{{NoInline, NoSpecialize}}
foo :: forall a. Show a => Int -> a -> String
foo 0 _ = "zero"
foo 1 _ = "one"
foo _ a = {{IgnoreWarning "DeprecatedFunction"}} showDeprecated a

data ColorEnum
  = {{Repr 0}} Red
  | {{Repr 1}} Green
  | {{Repr 2}} Blue

(Design notes: my main concern with picking a concrete syntax for annotations is making it unlikely to collide with other grammar elements now or in the future, as the grammar evolves. A @{Annotation} syntax, for example, would collide with type applications, since { can start a type. The previously-proposed @[Annotation] syntax doesn't currently cause problems, but might if type-level arrays are ever a thing. In contrast, at both the type and term levels, {{ is not a sequence of tokens that currently parses to anything, nor does it suggest a future language feature—curly braces are currently used exclusively for record terms and types, and one record literal or type can't start with another. Also, it's suggestive of block comment {- -} syntax, as befits something that straddles the line between commentary and code.)

Semantics

The compiler is permitted to use annotations as advice to make internal decisions that do not affect which programs are accepted.

Examples of things that a compiler may do with an annotation:

  • Ignore it
  • Enable or disable a warning
  • Enable or disable an optimization
  • Change how documentation outputs are generated
  • Change a type's run-time representation in a way that is not ordinarily visible from the rest of the language
  • Emit code coverage instrumentation, or change how such instrumentation is emitted
  • Write extra data to a file path that isn't confusable with codegen output
  • Specialize a function or module when a particular set of conditions is met (type arguments, backend, etc.)

Examples of things that a compiler may not do with an annotation:

  • Generate code that, if missing, would cause a program not to compile or to run incorrectly (sorry, deriving via)
  • Redirect a function or module to an implementation without which the function would not compile or run correctly
  • Transform type signatures
  • Throw an error (unless the annotation doesn't check; see below)

Alternate backends and consumers of CoreFn are recommended to adhere to the same guidelines when consuming annotations.

The compiler will assume that any programs using annotations contain (reference) a module called PureScript.Annotations (bikeshedding welcome), containing a type Annotation :: Type.

(We'll add such a module to the prelude. It may also contain some basic annotation types such as the below.)

Annotations are parsed, name checked, and type checked as expressions of type Annotation, with one important modification: the head of an annotation (Deprecated, for example) must be a ProperName, and it is desugared to (_ :: Deprecated)—in other words, annotation heads look and act like constructors but are name-checked as types. So the annotations in the above example assumes that the following have been declared and imported:

type Deprecated = String -> Annotation
type NoInline = Annotation
type NoSpecialize = Annotation
type IgnoreWarning = String -> Annotation

In more sophisticated cases, polymorphism and type classes can be used to constrain and validate the arguments to an annotation head.

An annotation that doesn't name check or type check is a compile-time error.

(Design notes: my hope is that annotations can be a rich field for experimentation without requiring participation from the compiler team to gatekeep them. At the same time, I want there to be some guardrails against users accidentally typoing their annotations or using them in unintended ways. That means making the annotation definitions user-definable, importable, and typed is a must. There's a choice here between defining annotations as term-like or type-like; I wanted to go with term-like, because I think PureScript's machinery for using type classes to direct type inference is more powerful at the term level than anything we currently have at the type level. But the trade-off is that annotations are irrelevant at run time, which suggests that they should be type-like; also, unless the compiler handles them specially, term-like annotation functions would need to have useless definitions attached even though only the type signatures are relevant. I settled on a desugaring compromise that might seem inelegant but should deliver the best ergonomics of both extremes.)

CoreFn output

Annotations are attached at parse time and the compiler makes a best effort to keep them attached until CoreFn is emitted. The compiler must not remove annotations from modules, named bindings (top-level or inner), or constructor definitions. The compiler may remove inline annotations if the expressions to which they are attached are mangled beyond recognition.

Annotations should be compiled to CoreFn the same way that expressions are, with annotation heads being represented as Var nodes that look like data constructors for Annotation (we shall all pretend to believe the fiction that Annotation is like an open data type, with every annotation type a new constructor for it). The top-level CoreFn Module, and the Ann attached to every CoreFn node, shall have a possibly-empty list of annotation Exprs added to it. Annotations appear in this list in the order in which they were written, but without paying attention to how many annotation groups were used; with this

{{Deprecated "use other thing instead"}}
{{NoInline, NoSpecialize}}
foo :: ...

foo will get the annotation list [App (Var `A.B.Deprecated`) (Literal "use other thing instead"), Var `A.B.NoInline`, Var `A.B.NoSpecialize`] (with lots of little irrelevant CoreFn details elided).

There may be more places in CoreFn that we want to add annotation data, to be determined as needs arise.

@natefaubion
Copy link
Contributor

In general, I think that's a really good proposal. A few questions:

Preceding a module declaration, on its own line

Is there an issue with scoping? For example, can you annotate a module with an annotation that's imported in the module? I don't see a technical limitation with this, other than it being a little odd.

Preceding an expr7 (atomic expressions, delimited expressions, and dotted chains), inline

Is this just to be conservative (ie, force parens to make it obvious what it applies to) or is there a limitation? If we supported expr5 you could annotate a do/ado expression as a whole (including the initial bind), otherwise you have to use parens. Record updates make things weird, I guess.

Preceding a typeAtom, inline

Are annotations made available in CoreFn for data type fields?

(with lots of little irrelevant CoreFn details elided).

To be clear, qualification is included in "CoreFn details"?

@rhendric
Copy link
Member

rhendric commented Jul 21, 2023

Preceding a module declaration, on its own line

Is there an issue with scoping? For example, can you annotate a module with an annotation that's imported in the module? I don't see a technical limitation with this, other than it being a little odd.

Yeah, I don't see a problem with it either, but I also don't think it's an essential case to support. I'd be inclined to say try it until it complicates things in which case don't. Edit: Oh wait, you said imported in the module; I was thinking defined in the module. Yeah, we do need to support that then.

Preceding an expr7 (atomic expressions, delimited expressions, and dotted chains), inline

Is this just to be conservative (ie, force parens to make it obvious what it applies to) or is there a limitation? If we supported expr5 you could annotate a do/ado expression as a whole (including the initial bind), otherwise you have to use parens. Record updates make things weird, I guess.

I was looking at record updates when I chose that, yeah. In principle I don't think there's an issue with letting keyword-initial productions also start with annotations; the way the grammar is currently set up I think it'd have to be added to those productions one by one if we don't want ambiguity with record updates, but that wouldn't be so bad (and maybe there's a clever reorg of the grammar I'm not seeing).

Preceding a typeAtom, inline

Are annotations made available in CoreFn for data type fields?

Good thought; I don't see why not.

(with lots of little irrelevant CoreFn details elided).

To be clear, qualification is included in "CoreFn details"?

Uh, yeah. I was confused here for a sec because Constructors don't contain qualified names, but that's because they aren't used for what I thought they're used for. I guess I mean those to be Vars with the IsConstructor meta. Whatever, key idea is, they're expressions and CoreFn consumers shouldn't need to build a whole new infrastructure to consume them.

@natefaubion
Copy link
Contributor

type Deprecated = String -> Annotation
type NoInline = Annotation
type NoSpecialize = Annotation
type IgnoreWarning = String -> Annotation

In more sophisticated cases, polymorphism and type classes can be used to constrain and validate the arguments to an annotation head.

Can you elaborate on this more? I don't really follow what you are envisioning regarding typeclasses, and why we should treat these type aliases somewhat magically rather than using foreign import data. I expect annotations to be a little niche, but I'm afraid that it might give a confusing intuition of type aliases to newcomers. It's basically overloading type aliase syntax to mean something completely different for the purposes of annotations only.

@rhendric
Copy link
Member

Sure, let's say someone wants to define an annotation that holds a record, and they want the labels to be arbitrary but all the values need to be String.

If you were trying to do this in executable code, you'd write something like this:

class StringRecordRL (l :: RowList Type)
instance StringRecordRL Nil
instance StringRecordRL tail => StringRecordRL (Cons s String tail)

acceptsStringRecord :: forall r l. RowToList r l => StringRecordRL l => Record r -> Unit
acceptsStringRecord _ = unit

As an annotation, instead, you'd write this:

class StringRecordRL (l :: RowList Type)
instance StringRecordRL Nil
instance StringRecordRL tail => StringRecordRL (Cons s String tail)

type AcceptsStringRecord = forall r l. RowToList r l => StringRecordRL l => Record r -> Annotation

And then the annotation, written {{AcceptsStringRecord { alpha: "some string" } }}, would be type checked as if it were the expression (?AcceptsStringRecord :: AcceptsStringRecord) { alpha: "some string" }.

If annotations were just types (defined with foreign import data or otherwise) instead of doing this annotation head overload thing, there'd be no way to express the intended constraint.

We could be less magic by dropping the constructor-like fiction and making annotations be real term declarations like

acceptsStringRecord :: forall r l. RowToList r l => StringRecordRL l => Record r -> Annotation
acceptsStringRecord _ = Annotation

I just don't like how verbose that is, or how it makes annotation functions look like they're meant to be evaluated at run time with other terms.

@natefaubion
Copy link
Contributor

I missed that the arguments are expr4. How does this interact with scoping (runtime arguments, type variables, given constraints)? I'm personally wary of using runtime syntax for this purpose. Would that be necessary if we had real data kinds?

@rhendric
Copy link
Member

How does this interact with scoping (runtime arguments, type variables, given constraints)?

I think there's a pretty straightforward right thing to do in all the places I'm proposing allowing annotations:

Uses the module-level scope to resolve names:

  • Preceding a module declaration, on its own line
  • Preceding any module-level declaration (including imports, fixity, etc.), on its own line

Uses the module-level scope plus any names made available in the parent context:

  • Preceding a class member, on its own line
  • Preceding an instance binding, on its own line
  • Preceding a data constructor definition, inline
  • Preceding a typeAtom, inline (when that type is part of a module-level declaration)

Uses the local scope that an expression in this position would use:

  • Preceding a let- (or where-) level declaration, on its own line
  • Preceding an expr7 (atomic expressions, delimited expressions, and dotted chains), inline
  • Preceding a typeAtom, inline (when that type is part of a let- or where-level declaration, a typed expression or binder, or a type application)

This is just a sketch but I don't see that much difficulty here; happy to discuss a specific example if you have one in mind.

One thing that I think is nice about this is that annotations get a sort of limited quotation capability for free. We can write, for example:

type Specialize :: forall a. a -> Annotation

{{Specialize fooInt}}
foo :: forall a. a -> Array a
foo = ...

fooInt :: Int -> Array Int
fooInt = ...

and even if the specialization takes place as a post-compiler transformation, the compiler can flag a typo while it does name checking.

Would that be necessary if we had real data kinds?

If we just had data kinds but not GADTs, I don't think we could do type class polymorphism tricks. If we had data kinds and GADTs but not quotation (or dependent types, I guess), we would have to use a string to name fooInt in the previous example. None of this stuff is necessary, though.

@natefaubion
Copy link
Contributor

If the annotation takes constraints, how does that elaborate in the CoreFn annotation syntax? Are constraints omitted or are they elaborated to annotation arguments? Is it useful to have them elaborated (ie, get a hold of a dictionary reference in an annotation)?

@rhendric
Copy link
Member

I don't have a specific use case in mind for using the dictionaries, but it might be useful for the compiler to solve for an instance dictionary expression in an annotation and then have a subsequent CoreFn transformation use that solved instance in some code that is being injected. On balance I think it's better to leave them in and ignore them than omit them and deviate from what CoreFn consumers already expect CoreFn to be able to contain.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

5 participants