Restricted Template Haskell

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

Restricted Template Haskell

Greg Weber
Hello GHC friends!

I am starting up a proposal for variants of Template Haskell that restrict what operations are available. The goal is to make TH easier for users to reason about and to allow for an easier compilation story.

Here is the proposal page:

Right now the proposal does not have any details and the goal is to write out a clear specification.
If this sounds interesting to you, let me know or leave some feedback on the wiki.


Thanks,
Greg Weber



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Restricted Template Haskell

Adam Vogt
Hi Greg,

Perhaps a less-invasive way to implement the -XSafe part of your
proposal would be to provide a module like:

module Language.Haskell.TH.Safe (
  module Language.Haskell.TH,
  reifyWithoutNameG,
 )  where
import Language.Haskell.TH hiding (runIO, reify*)

where reifyWithoutNameG is the same as reify, except definitions that
are out of scope are either missing or modified such that they use
NameQ instead of NameG for out-of-scope names.

That way there is no new syntax needed, and safe TH can be called by
unsafe TH without any conversions.

I think defining another monad like Q that can do less is too
inconvenient because you have to disambiguate between Safe.listE and
Unsafe.listE, or make those functions more polymorphic (which makes
type errors worse). Another option would be if there were

newtype QThat (canIO :: Bool) (canReify :: Bool) (canNewName :: Bool)
   = QThat (TheRealQImplementation)

type Q = QThat True True True

listE :: Monad m => [m Exp] -> m Exp
listE = liftM ListE . sequence

reify :: Name -> QThat a True b Info
runIO :: IO a -> QThat True b c a

runQFFF :: QThat False False False a -> a
runQTFF :: QThat True False False a -> IO a


But I think that design would be a step in the direction of "harder to
reason about"

Regards,
Adam


On Fri, Jan 30, 2015 at 6:39 PM, Greg Weber <[hidden email]> wrote:

> Hello GHC friends!
>
> I am starting up a proposal for variants of Template Haskell that restrict
> what operations are available. The goal is to make TH easier for users to
> reason about and to allow for an easier compilation story.
>
> Here is the proposal page:
> https://ghc.haskell.org/trac/ghc/wiki/TemplateHaskell/Restricted
>
> Right now the proposal does not have any details and the goal is to write
> out a clear specification.
> If this sounds interesting to you, let me know or leave some feedback on the
> wiki.
>
>
> Thanks,
> Greg Weber
>
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Restricted Template Haskell

Greg Weber


On Fri, Jan 30, 2015 at 7:05 PM, adam vogt <[hidden email]> wrote:
Hi Greg,

Perhaps a less-invasive way to implement the -XSafe part of your
proposal would be to provide a module like:

module Language.Haskell.TH.Safe (
  module Language.Haskell.TH,
  reifyWithoutNameG,
 )  where
import Language.Haskell.TH hiding (runIO, reify*)

where reifyWithoutNameG is the same as reify, except definitions that
are out of scope are either missing or modified such that they use
NameQ instead of NameG for out-of-scope names.

Thanks, I added this concept to the wiki.


That way there is no new syntax needed, and safe TH can be called by
unsafe TH without any conversions.

I think defining another monad like Q that can do less is too
inconvenient because you have to disambiguate between Safe.listE and
Unsafe.listE, or make those functions more polymorphic (which makes
type errors worse). Another option would be if there were

Oh, you are getting into more concrete details now than I have even thought about!
For the restricted monad route, we might look into a more capable method of using capabilities that would end up looking like this:

reify :: Name -> Restrict (TH :+: Reify) Info
runIO :: IO a -> Restrict (TH :+: RunIO) a

There are still a lot of details to work out, thanks for getting things started.

_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: Restricted Template Haskell

Simon Peyton Jones
In reply to this post by Greg Weber

The new TH is already split into two parts as I’m sure you know

·         Typed TH is for expressions only, and doesn’t have reify, nor any Q monad.

·         Untyped TH is the wild west

 

Typed TH may get some of what you want?   Certainly you want to acknowledge the existing split in your own design.

 

The proposal could do with examples to illustrate what the difficulties are.  What bad things happen in the Q monad?  Can you give examples of reasoning that would be valid in level 1 but not in level 2.  etc.  More precision please!

 

Simon

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Greg Weber
Sent: 30 January 2015 23:39
To: [hidden email]; GHC users
Cc: David Terei; Maxwell Swadling
Subject: Restricted Template Haskell

 

Hello GHC friends!

 

I am starting up a proposal for variants of Template Haskell that restrict what operations are available. The goal is to make TH easier for users to reason about and to allow for an easier compilation story.

 

Here is the proposal page:

 

Right now the proposal does not have any details and the goal is to write out a clear specification.

If this sounds interesting to you, let me know or leave some feedback on the wiki.

 

 

Thanks,

Greg Weber

 

 


_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Restricted Template Haskell

Greg Weber
Hi Simon,

I am just starting the proposal: gathering interested parties and pointers to related information.
Thanks for the pointer to Typed Template Haskell. I was actually unaware of the extent to which Typed Template Haskell is restricted. I have not seen any usage of Typed Template Haskell in the wild or been able to use it myself unfortunately due to backwards compatibility needs (once the next GHC release is out libraries will start to consider dropping 7.6 support and we will see more usage, although Ubuntu still ships 7.6 by default).
I will study Typed Template Haskell.

Greg Weber

On Mon, Feb 2, 2015 at 9:33 AM, Simon Peyton Jones <[hidden email]> wrote:

The new TH is already split into two parts as I’m sure you know

·         Typed TH is for expressions only, and doesn’t have reify, nor any Q monad.

·         Untyped TH is the wild west

 

Typed TH may get some of what you want?   Certainly you want to acknowledge the existing split in your own design.

 

The proposal could do with examples to illustrate what the difficulties are.  What bad things happen in the Q monad?  Can you give examples of reasoning that would be valid in level 1 but not in level 2.  etc.  More precision please!

 

Simon

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Greg Weber
Sent: 30 January 2015 23:39
To: [hidden email]; GHC users
Cc: David Terei; Maxwell Swadling
Subject: Restricted Template Haskell

 

Hello GHC friends!

 

I am starting up a proposal for variants of Template Haskell that restrict what operations are available. The goal is to make TH easier for users to reason about and to allow for an easier compilation story.

 

Here is the proposal page:

 

Right now the proposal does not have any details and the goal is to write out a clear specification.

If this sounds interesting to you, let me know or leave some feedback on the wiki.

 

 

Thanks,

Greg Weber

 

 



_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

Re: Restricted Template Haskell

Greg Weber
I would like to figure out how to improve the state of TTH documentation. The GHC wiki is usually for things that are changing, and the page is written in that future style, so it makes one wonder if all things are finished or if some things remain unfinished. Some "this is how it is" documentation in the user guide would seem more useful now.

But I am not sure if the user guide [1] is even correct because it indicates a type of `Q (TExp a)` where I would expect just `TExp a` from reading the wiki [2].


On Mon, Feb 2, 2015 at 11:31 AM, Greg Weber <[hidden email]> wrote:
Hi Simon,

I am just starting the proposal: gathering interested parties and pointers to related information.
Thanks for the pointer to Typed Template Haskell. I was actually unaware of the extent to which Typed Template Haskell is restricted. I have not seen any usage of Typed Template Haskell in the wild or been able to use it myself unfortunately due to backwards compatibility needs (once the next GHC release is out libraries will start to consider dropping 7.6 support and we will see more usage, although Ubuntu still ships 7.6 by default).
I will study Typed Template Haskell.

Greg Weber

On Mon, Feb 2, 2015 at 9:33 AM, Simon Peyton Jones <[hidden email]> wrote:

The new TH is already split into two parts as I’m sure you know

·         Typed TH is for expressions only, and doesn’t have reify, nor any Q monad.

·         Untyped TH is the wild west

 

Typed TH may get some of what you want?   Certainly you want to acknowledge the existing split in your own design.

 

The proposal could do with examples to illustrate what the difficulties are.  What bad things happen in the Q monad?  Can you give examples of reasoning that would be valid in level 1 but not in level 2.  etc.  More precision please!

 

Simon

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Greg Weber
Sent: 30 January 2015 23:39
To: [hidden email]; GHC users
Cc: David Terei; Maxwell Swadling
Subject: Restricted Template Haskell

 

Hello GHC friends!

 

I am starting up a proposal for variants of Template Haskell that restrict what operations are available. The goal is to make TH easier for users to reason about and to allow for an easier compilation story.

 

Here is the proposal page:

 

Right now the proposal does not have any details and the goal is to write out a clear specification.

If this sounds interesting to you, let me know or leave some feedback on the wiki.

 

 

Thanks,

Greg Weber

 

 




_______________________________________________
Glasgow-haskell-users mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Reply | Threaded
Open this post in threaded view
|

RE: Restricted Template Haskell

Simon Peyton Jones

Greg (and everyone else)

 

The TH documentation is even more woeful than I realised.  At the very least there should be a section for typed TH and a section for untyped TH in the manual.

 

If I volunteer to write it, it won’t get done.  I’m in too many inner loops.

 

But here’s an offer: if someone (or a little group) is willing to play author, I will review and correct. It could be a good way to learn the details!

 

Ideally it would be good to have a compact specification in the user manual, with more detail on the Haskell wiki (where it’s easier for people to edit/improve).  For the latter there is already a page here.

 

I’d really appreciate help with this. 

 

Simon

 

From: Greg Weber [mailto:[hidden email]]
Sent: 03 February 2015 03:42
To: Simon Peyton Jones
Cc: [hidden email]; GHC users; David Terei; Maxwell Swadling
Subject: Re: Restricted Template Haskell

 

I would like to figure out how to improve the state of TTH documentation. The GHC wiki is usually for things that are changing, and the page is written in that future style, so it makes one wonder if all things are finished or if some things remain unfinished. Some "this is how it is" documentation in the user guide would seem more useful now.

 

But I am not sure if the user guide [1] is even correct because it indicates a type of `Q (TExp a)` where I would expect just `TExp a` from reading the wiki [2].

 

 

On Mon, Feb 2, 2015 at 11:31 AM, Greg Weber <[hidden email]> wrote:

Hi Simon,

 

I am just starting the proposal: gathering interested parties and pointers to related information.

Thanks for the pointer to Typed Template Haskell. I was actually unaware of the extent to which Typed Template Haskell is restricted. I have not seen any usage of Typed Template Haskell in the wild or been able to use it myself unfortunately due to backwards compatibility needs (once the next GHC release is out libraries will start to consider dropping 7.6 support and we will see more usage, although Ubuntu still ships 7.6 by default).

I will study Typed Template Haskell.

 

Greg Weber

 

On Mon, Feb 2, 2015 at 9:33 AM, Simon Peyton Jones <[hidden email]> wrote:

The new TH is already split into two parts as I’m sure you know

·         Typed TH is for expressions only, and doesn’t have reify, nor any Q monad.

·         Untyped TH is the wild west

 

Typed TH may get some of what you want?   Certainly you want to acknowledge the existing split in your own design.

 

The proposal could do with examples to illustrate what the difficulties are.  What bad things happen in the Q monad?  Can you give examples of reasoning that would be valid in level 1 but not in level 2.  etc.  More precision please!

 

Simon

 

From: Glasgow-haskell-users [mailto:[hidden email]] On Behalf Of Greg Weber
Sent: 30 January 2015 23:39
To: [hidden email]; GHC users
Cc: David Terei; Maxwell Swadling
Subject: Restricted Template Haskell

 

Hello GHC friends!

 

I am starting up a proposal for variants of Template Haskell that restrict what operations are available. The goal is to make TH easier for users to reason about and to allow for an easier compilation story.

 

Here is the proposal page:

 

Right now the proposal does not have any details and the goal is to write out a clear specification.

If this sounds interesting to you, let me know or leave some feedback on the wiki.

 

 

Thanks,

Greg Weber

 

 

 

 


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