Getting both the value and name of a variable in one expression

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

Getting both the value and name of a variable in one expression

Christopher Done-2

Hi all,

Do we have already a syntax for ‘foo that also contains the typed value like TExp?

I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:

-- | Check the grammar spec to produce a grammar.
checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
checkGrammar (toplevel, rules) =
  if M.size rulesMap /= length rules
    then error "Duplicate rule names in grammar."
    else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
  where
    rulesMap = M.fromList rules

-- | Grammar for Haskell.
grammar :: Grammar
grammar = $(checkGrammar $ runDefine $ mdo
  -- General expression
  expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
                                                      ,tuple, let', application, string])
  application      <- rule "Application" (CompositeSchema [expression, expression])
  parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])

...
 pure expression)

Here I do a trivial check for duplicates. After I’ve checked the
expression at compile-time, I Lift it so that it can be used at
runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
an alternative would be:

grammar = $(checkGrammar_take2 thename 'thename)

In which checkGrammar_take2 would:

  1. Use thename at compile-time for a check.
  2. If the check passes, then return (VarE thename)

E.g.

checkGrammar_take2 value name = if valueFine value then varE name else
error "value isn't fine"

That’s actually quite a good solution because it avoids a lift, and I
didn’t transform the AST. It’s also more efficient than lifting.

But there’s no checked relationship between thename and ‘thename.
checkGrammar_take2 has no way of knowing that they refer to the same
thing. See?

Hence, if I could get e.g. `thename to produce both the value and a
name for the value, that would be cool. My gist doesn’t go this
far. It might look like this:

checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"

and call it like:

mygrammar = checkGrammar_take2 `thename

So the semantics would be roughly similar to

[|| thename ||] :: TExp a

but you’d get

`thename :: Named a

where

data Named a = { namedThing :: a, nameOfThing :: Name }

I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.

Cheers,

Chris


_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Michael Sloan
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:

>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Christopher Done-2
I considered an expression-within-an-expression but thought a stage-restriction would break it. Maybe not! Let me go test it!

On Wed, 21 Aug 2019 at 17:31, Michael Sloan <[hidden email]> wrote:
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:
>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Christopher Done-2

Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH.Syntax
import Language.Haskell.TH
import Language.Haskell.TH.Lift ()

valueFine :: String -> Bool
valueFine = not . null

checkGrammar_2 :: Name -> ExpQ
checkGrammar_2 name =
  [| if valueFine $(varE name)
      then varE name
      else error "value isn't fine" |]

thename :: [Char]
thename = "Hello!"

thename_empty :: [Char]
thename_empty = ""

The output:

> :t $(checkGrammar_2 'thename)
$(checkGrammar_2 'thename) :: ExpQ
> :t $($(checkGrammar_2 'thename))
$($(checkGrammar_2 'thename)) :: [Char]
> $($(checkGrammar_2 'thename))
"Hello!"
> $($(checkGrammar_2 'thename_empty))

<interactive>:49:1: error:
    • Exception when trying to run compile-time code:
        value isn't fine
CallStack (from HasCallStack):
  error, called at <interactive>:49:5 in interactive:Ghci2
      Code: (if valueFine thename_empty then
                 varE
                   ((Name (mkOccName "thename_empty"))
                      (((NameG VarName) (mkPkgName "main")) (mkModName "Main")))
             else
                 error "value isn't fine")
    • In the untyped splice: $($(checkGrammar_2 'thename_empty))

Thanks Michael! You’re a star!

I should document this in a gist or blog post or something as a technique for DSL checking.


On Thu, 22 Aug 2019 at 16:26, Christopher Done <[hidden email]> wrote:
I considered an expression-within-an-expression but thought a stage-restriction would break it. Maybe not! Let me go test it!

On Wed, 21 Aug 2019 at 17:31, Michael Sloan <[hidden email]> wrote:
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:
>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Christopher Done-2

Depending on how much syntactic overhead you’re happy with, you can go full type-safe:

checkGrammar_3 :: Q (TExp String) -> Q (TExp (Q (TExp String)))
checkGrammar_3 q = do
  TExp expr <- q
  [|| if valueFine $$(q)
      then pure (TExp expr)
      else error "value is not fine" ||]
> $$($$(checkGrammar_3 [|| thename ||]))
"Hello!"
> $$($$(checkGrammar_3 [|| thename_empty ||]))

<interactive>:45:4: error:
    • Exception when trying to run compile-time code:
        value is not fine

In my case it might even be a fine trade-off, because I’m favoring TH-based validation of a DSL where doing it with e.g. type-level lists and type families has worse type-inference and a higher price to pay in type-signatures. So I can make a “static-smart” constructor that looks more like:

checkGrammar_3 :: Q (TExp (Tree a)) -> Q (TExp (Q (TExp (ValidTree a))))
useValidTree :: ValidTree a -> ...

So you pay the cost once here, but when building the tree, which is more larger code, you don’t pay any cost, and there’s where it matters.


On Thu, 22 Aug 2019 at 16:40, Christopher Done <[hidden email]> wrote:

Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH.Syntax
import Language.Haskell.TH
import Language.Haskell.TH.Lift ()

valueFine :: String -> Bool
valueFine = not . null

checkGrammar_2 :: Name -> ExpQ
checkGrammar_2 name =
  [| if valueFine $(varE name)
      then varE name
      else error "value isn't fine" |]

thename :: [Char]
thename = "Hello!"

thename_empty :: [Char]
thename_empty = ""

The output:

> :t $(checkGrammar_2 'thename)
$(checkGrammar_2 'thename) :: ExpQ
> :t $($(checkGrammar_2 'thename))
$($(checkGrammar_2 'thename)) :: [Char]
> $($(checkGrammar_2 'thename))
"Hello!"
> $($(checkGrammar_2 'thename_empty))

<interactive>:49:1: error:
    • Exception when trying to run compile-time code:
        value isn't fine
CallStack (from HasCallStack):
  error, called at <interactive>:49:5 in interactive:Ghci2
      Code: (if valueFine thename_empty then
                 varE
                   ((Name (mkOccName "thename_empty"))
                      (((NameG VarName) (mkPkgName "main")) (mkModName "Main")))
             else
                 error "value isn't fine")
    • In the untyped splice: $($(checkGrammar_2 'thename_empty))

Thanks Michael! You’re a star!

I should document this in a gist or blog post or something as a technique for DSL checking.


On Thu, 22 Aug 2019 at 16:26, Christopher Done <[hidden email]> wrote:
I considered an expression-within-an-expression but thought a stage-restriction would break it. Maybe not! Let me go test it!

On Wed, 21 Aug 2019 at 17:31, Michael Sloan <[hidden email]> wrote:
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:
>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Christopher Done-2
Wrote up here! https://chrisdone.com/posts/static-smart-constructors/

This was totally blocking my library from becoming complete, I'm super happy I can proceed now.

On Thu, 22 Aug 2019 at 17:09, Christopher Done <[hidden email]> wrote:

Depending on how much syntactic overhead you’re happy with, you can go full type-safe:

checkGrammar_3 :: Q (TExp String) -> Q (TExp (Q (TExp String)))
checkGrammar_3 q = do
  TExp expr <- q
  [|| if valueFine $$(q)
      then pure (TExp expr)
      else error "value is not fine" ||]
> $$($$(checkGrammar_3 [|| thename ||]))
"Hello!"
> $$($$(checkGrammar_3 [|| thename_empty ||]))

<interactive>:45:4: error:
    • Exception when trying to run compile-time code:
        value is not fine

In my case it might even be a fine trade-off, because I’m favoring TH-based validation of a DSL where doing it with e.g. type-level lists and type families has worse type-inference and a higher price to pay in type-signatures. So I can make a “static-smart” constructor that looks more like:

checkGrammar_3 :: Q (TExp (Tree a)) -> Q (TExp (Q (TExp (ValidTree a))))
useValidTree :: ValidTree a -> ...

So you pay the cost once here, but when building the tree, which is more larger code, you don’t pay any cost, and there’s where it matters.


On Thu, 22 Aug 2019 at 16:40, Christopher Done <[hidden email]> wrote:

Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH.Syntax
import Language.Haskell.TH
import Language.Haskell.TH.Lift ()

valueFine :: String -> Bool
valueFine = not . null

checkGrammar_2 :: Name -> ExpQ
checkGrammar_2 name =
  [| if valueFine $(varE name)
      then varE name
      else error "value isn't fine" |]

thename :: [Char]
thename = "Hello!"

thename_empty :: [Char]
thename_empty = ""

The output:

> :t $(checkGrammar_2 'thename)
$(checkGrammar_2 'thename) :: ExpQ
> :t $($(checkGrammar_2 'thename))
$($(checkGrammar_2 'thename)) :: [Char]
> $($(checkGrammar_2 'thename))
"Hello!"
> $($(checkGrammar_2 'thename_empty))

<interactive>:49:1: error:
    • Exception when trying to run compile-time code:
        value isn't fine
CallStack (from HasCallStack):
  error, called at <interactive>:49:5 in interactive:Ghci2
      Code: (if valueFine thename_empty then
                 varE
                   ((Name (mkOccName "thename_empty"))
                      (((NameG VarName) (mkPkgName "main")) (mkModName "Main")))
             else
                 error "value isn't fine")
    • In the untyped splice: $($(checkGrammar_2 'thename_empty))

Thanks Michael! You’re a star!

I should document this in a gist or blog post or something as a technique for DSL checking.


On Thu, 22 Aug 2019 at 16:26, Christopher Done <[hidden email]> wrote:
I considered an expression-within-an-expression but thought a stage-restriction would break it. Maybe not! Let me go test it!

On Wed, 21 Aug 2019 at 17:31, Michael Sloan <[hidden email]> wrote:
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:
>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.
Reply | Threaded
Open this post in threaded view
|

Re: Getting both the value and name of a variable in one expression

Michael Sloan
Awesome Chris, glad the idea was applicable!

Nice post on the topic, I hadn't thought of using this for more powerful validation of values.  Use of quasiquotes and such for validated literals is well known, but this approach allows compiletime validation of the results of arbitrary expressions and not just strings!  Very cool.

On Thu, Aug 22, 2019 at 10:49 AM Christopher Done <[hidden email]> wrote:
Wrote up here! https://chrisdone.com/posts/static-smart-constructors/

This was totally blocking my library from becoming complete, I'm super happy I can proceed now.

On Thu, 22 Aug 2019 at 17:09, Christopher Done <[hidden email]> wrote:

Depending on how much syntactic overhead you’re happy with, you can go full type-safe:

checkGrammar_3 :: Q (TExp String) -> Q (TExp (Q (TExp String)))
checkGrammar_3 q = do
  TExp expr <- q
  [|| if valueFine $$(q)
      then pure (TExp expr)
      else error "value is not fine" ||]
> $$($$(checkGrammar_3 [|| thename ||]))
"Hello!"
> $$($$(checkGrammar_3 [|| thename_empty ||]))

<interactive>:45:4: error:
    • Exception when trying to run compile-time code:
        value is not fine

In my case it might even be a fine trade-off, because I’m favoring TH-based validation of a DSL where doing it with e.g. type-level lists and type families has worse type-inference and a higher price to pay in type-signatures. So I can make a “static-smart” constructor that looks more like:

checkGrammar_3 :: Q (TExp (Tree a)) -> Q (TExp (Q (TExp (ValidTree a))))
useValidTree :: ValidTree a -> ...

So you pay the cost once here, but when building the tree, which is more larger code, you don’t pay any cost, and there’s where it matters.


On Thu, 22 Aug 2019 at 16:40, Christopher Done <[hidden email]> wrote:

Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}
import Language.Haskell.TH.Syntax
import Language.Haskell.TH
import Language.Haskell.TH.Lift ()

valueFine :: String -> Bool
valueFine = not . null

checkGrammar_2 :: Name -> ExpQ
checkGrammar_2 name =
  [| if valueFine $(varE name)
      then varE name
      else error "value isn't fine" |]

thename :: [Char]
thename = "Hello!"

thename_empty :: [Char]
thename_empty = ""

The output:

> :t $(checkGrammar_2 'thename)
$(checkGrammar_2 'thename) :: ExpQ
> :t $($(checkGrammar_2 'thename))
$($(checkGrammar_2 'thename)) :: [Char]
> $($(checkGrammar_2 'thename))
"Hello!"
> $($(checkGrammar_2 'thename_empty))

<interactive>:49:1: error:
    • Exception when trying to run compile-time code:
        value isn't fine
CallStack (from HasCallStack):
  error, called at <interactive>:49:5 in interactive:Ghci2
      Code: (if valueFine thename_empty then
                 varE
                   ((Name (mkOccName "thename_empty"))
                      (((NameG VarName) (mkPkgName "main")) (mkModName "Main")))
             else
                 error "value isn't fine")
    • In the untyped splice: $($(checkGrammar_2 'thename_empty))

Thanks Michael! You’re a star!

I should document this in a gist or blog post or something as a technique for DSL checking.


On Thu, 22 Aug 2019 at 16:26, Christopher Done <[hidden email]> wrote:
I considered an expression-within-an-expression but thought a stage-restriction would break it. Maybe not! Let me go test it!

On Wed, 21 Aug 2019 at 17:31, Michael Sloan <[hidden email]> wrote:
One potential solution here is to have checkGrammar_take2 return an
expression which returns an expression.  I haven't tried compiling
this, but something roughly like:

checkGrammar_2 name = [| if valueFine $(varE name) then varE name else
error "value isn't fine" |]

Then it'd be used like $($(checkGrammar_2 'thename)).  The th-orphans
package can also be useful for this because it provides Lift instances
for the TH AST.

-Michael

On Tue, Aug 20, 2019 at 10:36 AM Christopher Done <[hidden email]> wrote:
>
> Hi all,
>
> Do we have already a syntax for ‘foo that also contains the typed value like TExp?
>
> I have e.g. an AST that I want to do more static checks on it that aren’t as convenient to do in the type system. Here’s an example:
>
> -- | Check the grammar spec to produce a grammar.
> checkGrammar :: (SchemaName, [(SchemaName, Schema)]) -> Q Exp
> checkGrammar (toplevel, rules) =
>   if M.size rulesMap /= length rules
>     then error "Duplicate rule names in grammar."
>     else lift (Grammar {grammarToplevel = toplevel, grammarRules = rulesMap})
>   where
>     rulesMap = M.fromList rules
>
> -- | Grammar for Haskell.
> grammar :: Grammar
> grammar = $(checkGrammar $ runDefine $ mdo
>   -- General expression
>   expression       <- rule "Expression" (ChoiceSchema [variable, constructor, parentheses
>                                                       ,tuple, let', application, string])
>   application      <- rule "Application" (CompositeSchema [expression, expression])
>   parentheses      <- rule "Parentheses" (CompositeSchema [openParenSchema, expression, closeParenSchema])
>
> ...
>  pure expression)
>
> Here I do a trivial check for duplicates. After I’ve checked the
> expression at compile-time, I Lift it so that it can be used at
> runtime. That’s pretty good. But some types like (a -> b) don’t Lift. So
> an alternative would be:
>
> grammar = $(checkGrammar_take2 thename 'thename)
>
> In which checkGrammar_take2 would:
>
> Use thename at compile-time for a check.
> If the check passes, then return (VarE thename)
>
> E.g.
>
> checkGrammar_take2 value name = if valueFine value then varE name else
> error "value isn't fine"
>
> That’s actually quite a good solution because it avoids a lift, and I
> didn’t transform the AST. It’s also more efficient than lifting.
>
> But there’s no checked relationship between thename and ‘thename.
> checkGrammar_take2 has no way of knowing that they refer to the same
> thing. See?
>
> Hence, if I could get e.g. `thename to produce both the value and a
> name for the value, that would be cool. My gist doesn’t go this
> far. It might look like this:
>
> checkGrammar_take2 namedValue = if valueFine (getValue namedValue) then getExp namedValue else error "value isn't fine"
>
> and call it like:
>
> mygrammar = checkGrammar_take2 `thename
>
> So the semantics would be roughly similar to
>
> [|| thename ||] :: TExp a
>
> but you’d get
>
> `thename :: Named a
>
> where
>
> data Named a = { namedThing :: a, nameOfThing :: Name }
>
> I feel like the more DSLs I design, the more I’d like something like this to perform my static checks.
>
> Cheers,
>
> Chris
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.

_______________________________________________
Haskell-Cafe mailing list
To (un)subscribe, modify options or view archives go to:
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Only members subscribed via the mailman list are allowed to post.