My personal desire, and this is just pie-in-the-sky-but-might-be-nice-extremely-long-term, would be to support lifting all core terms to the type level as is, so that they could be reflected/reified, with goal of supporting compile-time evaluation of some kind. I doubt other maintainers agree 
. But I think if we want different numeric types, we should keep the possibility of supporting them at both the type and term level, and they should have consistent syntax. I don’t really want Int literals to mean something else at the type level.
2 Likes
I would see the benefit of having an extensible annotation syntax. I’d argue for a row type where the labels denote the annotations the compiler currently understands. The ones the compiler doesn’t know about would be dropped for forward compatibility. With an optional warning flag.
@(layout :: Unpack, roles :: [Nominal], derive :: [Eq, Ord], deriveVia :: ( via :: Bar, targets :: [Show] ) ]
data Foo a = ...
@( deprecated :: "Use `bar` instead" )
foo :: a -> Foo a
foo = ...
I’m wondering if it’d be possible to remove the need for typelevel lists, so it’d be possible to implement faster. roles could probably be changed to a record via
@(roles :: (nominal :: True) )
But I don’t see such an option for derive, which would imo be the main driver here. We could hack something akin to
@( derive :: (eq: Eq, show: Show) )
And ignore the labels. Ugly, but should work. Upgrading once the “real” [] syntax shows up should be possible with some compiler magic.
4 Likes
I don’t think adding syntax and kind-checker support for arrays, booleans, etc would be particularly difficult. The only thing that’s difficult is if we expect solver support for operations on type-level arrays, which is not necessary for annotations.
2 Likes
Really like your thinking! Rows for the win!
1 Like
GHC has accepted a very similar proposal for “modifiers”, with similar motivating examples.
6 Likes
If I understand correctly, they are ment to modify the next token in a type signature or type declaration. This is totally useful for the multiplicity and matchability of arrows, or for roles of type variables. But how does it fit, for example, a deprecation annotation? Or a derive directive? Both are annotations on declarations not on a particular part of a type…
1 Like
I don’t think it’s explicitly only in a type declaration.
Modifiers somehow change the meaning of the next token or of the construct they appear in. The
blahis parsed and renamed as a type.
My interpretation of that is that it can be used anywhere, while using the type language as the “syntax”.
data Foo (%Nominal a) = ...
Seems natural. But how would you use modifiers to annotate deprecation of a function? Something like this is?
%(Deprecated "Use g instead") f :: a -> b -> c
Where the modifier is attached to f? Seems OK. Or whole data type?
data %(Deprecated "Use Bar instead") Foo (%Nominal a) = ...
Because the modifier is on Foo?
That’s rather ugly read I think. For what it’s worth, I’d highly prefer to separate annotations from the type language, as type signatures are separated from function declarations:
@[roles [Nominal]]
data Foo a = ...
@[deprecated "Use g instead"]
f :: a -> b -> c
f x y = ...
2 Likes
I should note that I’m not in any way saying we should follow GHC’s lead exactly. I’m just pointing it out as a reference that something very similar has already been proposed and accepted, with similar motivating examples.
4 Likes