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 <chrisdone@gmail.com> 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 <chrisdone@gmail.com> 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 <chrisdone@gmail.com> 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 <mgsloan@gmail.com> 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 <chrisdone@gmail.com> 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.