Implement TypeSignatureSections
Needs RevisionPublic

Authored by hvr on Aug 28 2015, 10:40 AM.

Details

Reviewers
simonpj
bgamari
austin
Trac Issues
#10803
Summary

This works mostly but I've got a problem stuffing a TcCoercion into a PostTc id Coercion.

See Trac #10803

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Branch
wip/T10803
Lint
Lint OK
Unit
No Unit Test Coverage
Build Status
Buildable 5419
Build 5788: GHC Patch Validation (amd64/Linux)
Build 5787: arc lint + arc unit
hvr updated this revision to Diff 3957.Aug 28 2015, 10:40 AM
hvr retitled this revision from to First part of implementing TypeSignatureSections.
hvr updated this object.
hvr edited the test plan for this revision. (Show Details)
hvr added reviewers: simonpj, bgamari.
hvr updated the Trac tickets for this revision.
hvr added a comment.EditedAug 28 2015, 10:49 AM

Here's how it currently behaves:

λ:11> :t (:: Maybe ())
(:: Maybe ()) :: Maybe () -> Maybe ()

λ:12> :t (:: a)
(:: a) :: (forall a. a) -> forall a. a

-- ^^ I'm not happy with this one above


λ:15> :t (show . (:: Int) . read)
(show . (:: Int) . read) :: String -> String


λ:16>  (show . (:: Int) . read) "  00123123123"
"123123123"
it :: String



λ:17> :t length 
length :: Foldable t => t a -> Int

λ:18> :t length . (:: [Int])
length . (:: [Int]) :: [Int] -> Int

λ:19> :t length . (:: [a])

<interactive>:1:11: error:
    Couldn't match type ‘forall a1. [a1]’ with ‘t0 a0’
    Expected type: a -> t0 a0
      Actual type: (forall a. [a]) -> forall a. [a]
    In the second argument of ‘(.)’, namely ‘(:: [a])’
    In the expression: length . (:: [a])

-- ^^ again, I'm not happy with this last one...


λ:21> (:: [_]) ("Hello" :: String)

<interactive>:21:6: error:
    Found type wildcard ‘_’ standing for ‘Char’
    To use the inferred type, enable PartialTypeSignatures
    Relevant bindings include it :: [Char] (bound at <interactive>:21:1)
    In an expression type signature: [_]
    In the expression: :: [_]
    In the expression: (:: [_]) ("Hello" :: String)



λ:22> (:: [a]) ("Hello" :: String)

<interactive>:22:11: error:
    Couldn't match type ‘a1’ with ‘Char’
    ‘a1’ is a rigid type variable bound by a type expected by the context: [a1] at <interactive>:22:1
    Expected type: [a1]
      Actual type: String
    In the first argument of ‘:: [a]’, namely ‘("Hello" :: String)’
    In the expression: (:: [a]) ("Hello" :: String)
    In an equation for ‘it’: it = (:: [a]) ("Hello" :: String)


-- ^^ :-(
hvr added inline comments.Aug 28 2015, 10:57 AM
compiler/deSugar/DsExpr.hs
280

I'm not even sure why I need the coercion at all though... :-)

compiler/typecheck/TcExpr.hs
381–382

Here's the constructur signature:

data HsExpr id = 
          -- ...
	  | TySigSectionOut (LHsType Name)
	                    (PostTc id Type)
	                    (PostTc id Coercion)

I've noticed there's a

dsTcCoercion :: TcCoercion -> (Coercion -> CoreExpr) -> DsM CoreExpr

operation, but this only works in the DsM monad, however, if I use a PostTc id TcCoercion for the field instead, I get deriving problems with the Data instance for HsExpr...

dolio added a subscriber: dolio.Aug 28 2015, 11:15 AM

The examples involving type variables are odd. They should probably be generalized as part of the type ascribed to the function, and not as the argument. I.E. right now we have:

(:: type) = \(x :: Generalize[type]) -> x

but we want something more like:

(:: type) = ((\(x :: type) -> x) :: Generalize[type -> type])
spl added a subscriber: spl.Aug 29 2015, 12:48 AM
mpickering added inline comments.Aug 29 2015, 12:10 PM
compiler/parser/Parser.y
2330

The location of :: needs to be saved.

Something like

{% ams (sLL $1 $> $ TySigSection $2 PlaceHolder) [mj AnnDcolon $1]}

should work.

Is there a wiki page for this proposal?

I agree that (:: a) :: (forall a. a) -> (forall a. a) is a bit strange. Note that if a were in scope, this generalization wouldn't happen. What is a use-case for using a not-in-scope type variable in a signature section? Perhaps the programmer would prefer a type wildcard instead (which should work out of the box, I think)? So maybe this isn't so bad, after all.

Would there be any runtime consequences of using this feature? Naively, it would seem so, as we're creating a new function and calling it. That would make me sad.

dolio added a comment.Aug 29 2015, 2:14 PM

I think I agree with Richard. I can't think of a reason to use (unbound) variables other than for them to work as wildcards. But we have wildcards. So perhaps the current behavior is okay, or should be an error, rather than what I suggested.

As for performance, assuming this did just turn into \(x :: ty) -> x, wouldn't the optimizer eliminate it?

hvr added a comment.EditedAug 30 2015, 4:09 AM
In D1185#33027, @dolio wrote:

I think I agree with Richard. I can't think of a reason to use (unbound) variables other than for them to work as wildcards. But we have wildcards. So perhaps the current behavior is okay, or should be an error, rather than what I suggested.

While trying out the implementation I was wondering if we don't want

(:: <type>)

to be mostly syntactic shorthand for the typed lambda abstraction

(\ ( x :: <type> ) -> x )

Allowing for things like (:: (a,a)) to mean

> :set -XScopedTypeVariables
> :t (\(x::(a,a)) -> x)
(\(x::(a,a)) -> x) :: (a, a) -> (a, a)

or things like (:: Exception e => Either e a) which can't be done with wildcards right now (as we don't have named wildcards at the type-level afaik).

hvr updated this revision to Diff 3979.Aug 30 2015, 4:11 AM
hvr edited edge metadata.
  • Attach location informaation
  • Add -XSignatureSections pragma
hvr marked an inline comment as done.Aug 30 2015, 4:12 AM
hvr added inline comments.
compiler/parser/Parser.y
2330

thanks, fixed

In D1185#33027, @dolio wrote:

As for performance, assuming this did just turn into \(x :: ty) -> x, wouldn't the optimizer eliminate it?

Are we sure this would always happen? What if we end up mapping the signature section? Or do other strange things with it? In any case, this should be tested.

In D1185#33035, @hvr wrote:

While trying out the implementation I was wondering if we don't want

(:: <type>)

to be mostly syntactic shorthand for the typed lambda abstraction

(\ ( x :: <type> ) -> x )

Would we enable -XScopedTypeVariables locally over the signature section? (I think we should, under this proposal.) But I actually prefer the wildcards approach. Note that, under the current implementation of ScopedTypeVariables, a scoped type variable may unify only with a variable never a known type. (For example, (\(x :: (a,a)) -> x) (True, False) does not type-check.) Also, with wildcards, the user can get feedback about what the correct type should be.

And, yes, I do believe we have named type wildcards, so your case with a repeated variable should be OK.

hvr marked an inline comment as done.Aug 31 2015, 1:09 AM

And, yes, I do believe we have named type wildcards, so your case with a repeated variable should be OK.

You're right! I forgot they need to be enabled separately via -XNamedWildCards. Also, Lennart is ok with not supporting free variables and doing a conservative implementation for now which can be extended later, his response to me was (assuming he's ok with me quoting him here) :

I'd say, make it as conservative as possible.
So I'd ban free type variables in the type. It's a restriction that can be relaxed if we want.
But I'm happy if you give it some other sensible semantics.

dolio added a comment.Aug 31 2015, 2:09 AM

Are we sure this would always happen? What if we end up mapping the signature section? Or do other strange things with it? In any case, this should be tested.

I'm not sure I understand what you're asking. No, map id isn't (in general) free, and neither is it if you replace id with a signature section. If these are expected to behave like first-class functions, then when used as such, there are potentially costs, just like there are with id.

Or are you worried that they are more costly than id?

simonpj edited edge metadata.Aug 31 2015, 8:58 AM

Good start.

Please make a wiki page to describe the design. There are, as you have discovered, always wrinkles.

I strongly agree (for now anyway) we should only allow a named type variable (like 'a') in a signature section if 'a' is lexically in scope from some enclosing construct. No implicit quantification! If you want wildcards use wildcards.

I have not yet looked at the code. Let's get the design agreed first.

Thanks for doing this.

Signature sections might be worse than id in at least two ways: 1) there might be RULES around id that wouldn't apply, and 2) a signature section would seem to allocate a new function instead of using an existing one. Both of these issues would be mitigated if (:: t) expanded to (id @t), where @t is a visible type application (see D1138).

But, to be honest, I'm not all that worried about being worse than id. I'm worried about being worse than a normal type signature -- that is, to have any runtime cost at all. Signature sections are meant as a light syntactic sugar, and they have appeal as such. But I would avoid them entirely if this light syntactic sugar cost me at runtime.

While I'm thinking about visible type application, once we have that feature, is this one needed any more? Do we have real-ish examples of when we want signature sections? The examples for http://augustss.blogspot.co.at/2014/04/a-small-haskell-extension.html are all quite easy to write with visible type application.

austin requested changes to this revision.Sep 23 2015, 3:52 AM
austin edited edge metadata.

(Marking as 'Request Changes' to bump out of the review queue.)

This revision now requires changes to proceed.Sep 23 2015, 3:52 AM
hvr retitled this revision from First part of implementing TypeSignatureSections to Implementing TypeSignatureSections.Dec 19 2015, 7:52 AM
hvr edited edge metadata.
hvr retitled this revision from Implementing TypeSignatureSections to Implement TypeSignatureSections.
alanz added a subscriber: alanz.Dec 19 2015, 8:12 AM
alanz added inline comments.
compiler/typecheck/TcExpr.hs
382

I hope the panic is temporary while this is under development, it should rather be a place holder type

austin resigned from this revision.Nov 6 2017, 10:10 PM