Why is EvTerm limited?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Why is EvTerm limited?

Joachim Breitner-2
Hi,

I had some funky idea where a type checker plugin would have to
synthesize code for a custom-solved instances on the fly. But it seems
that does not work because EvTerm is less expressive than Core
(especially, no lambdas):
https://downloads.haskell.org/~ghc/8.2.2/docs/html/libraries/ghc-8.2.2/TcEvidence.html#t:EvTerm

What would break if we had

 | EvExpr CoreExpr

as an additional constructor there?

Cheers,
Joachim

--
Joachim “nomeata” Breitner
  [hidden email]
  https://www.joachim-breitner.de/

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

RE: Why is EvTerm limited?

Haskell - Glasgow-haskell-users mailing list
|  What would break if we had
|  
|   | EvExpr CoreExpr
|  
|  as an additional constructor there?

This has come up before.  I think that'd be a solid win.

In fact, eliminate all the existing evidence constructors with "smart constructors" that produce an EvExpr.  That'd mean moving stuff from the desugarer into these smart constructors, but that's ok.

I /think/ I didn't do that initially only because there were very few forms and it mean that there was no CoreExpr stuff in the type checker. But as we add more forms that decision looks and less good.

You'd need to add zonkCoreExpr in place of zonkEvTerm.

evVarsOfTerm is called quite a bit; you might want to cache the result in the EvExpr constructor.

Make a ticket and execute?

Simon

|  -----Original Message-----
|  From: Glasgow-haskell-users [mailto:glasgow-haskell-users-
|  [hidden email]] On Behalf Of Joachim Breitner
|  Sent: 19 January 2018 14:01
|  To: Glasgow-Haskell-Users users <[hidden email]>
|  Subject: Why is EvTerm limited?
|  
|  Hi,
|  
|  I had some funky idea where a type checker plugin would have to
|  synthesize code for a custom-solved instances on the fly. But it seems
|  that does not work because EvTerm is less expressive than Core
|  (especially, no lambdas):
|  https://na01.safelinks.protection.outlook.com/?url=https:%2F%2Fdownloa
|  ds.haskell.org%2F~ghc%2F8.2.2%2Fdocs%2Fhtml%2Flibraries%2Fghc-
|  8.2.2%2FTcEvidence.html%23t:EvTerm&data=02%7C01%7Csimonpj%40microsoft.
|  com%7C513ff7ae83914913225008d55f452dec%7C72f988bf86f141af91ab2d7cd011d
|  b47%7C1%7C0%7C636519673089385423&sdata=kFkUugVn02Nfu4QXJ6dkVwtx8KWFrTM
|  fWcVEiwf6KyI%3D&reserved=0
|  
|  What would break if we had
|  
|   | EvExpr CoreExpr
|  
|  as an additional constructor there?
|  
|  Cheers,
|  Joachim
|  
|  --
|  Joachim “nomeata” Breitner
|    [hidden email]
|  
|  https://na01.safelinks.protection.outlook.com/?url=https%3A%2F%2Fwww.j
|  oachim-
|  breitner.de%2F&data=02%7C01%7Csimonpj%40microsoft.com%7C513ff7ae839149
|  13225008d55f452dec%7C72f988bf86f141af91ab2d7cd011db47%7C1%7C0%7C636519
|  673089385423&sdata=Vh4BvbeEVUBIntKcf3XEseOzwUTx2RHPuANTY328dpM%3D&rese
|  rved=0
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users