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

older
Question on inductive type-families

Christopher Done

20 Aug 2019 20 Aug '19

12:36 p.m.

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 ExpcheckGrammar (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 :: Grammargrammar = $(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 elseerror "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

Attachments:

attachment.html (text/html — 15.6 KB)

Show replies by date

Michael Sloan

21 Aug 21 Aug

12:31 p.m.

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

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 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.

Christopher Done

22 Aug 22 Aug

11:26 a.m.

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

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 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 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 =

...
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

rulesMap}) 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.

Christopher Done

11:40 a.m.

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

Hurray! It works! {-# LANGUAGE TemplateHaskell #-}import Language.Haskell.TH.Syntaximport Language.Haskell.THimport Language.Haskell.TH.Lift () valueFine :: String -> BoolvalueFine = not . null checkGrammar_2 :: Name -> ExpQcheckGrammar_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 fineCallStack (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 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 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 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 =

...
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

rulesMap}) 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.

Christopher Done

12:09 p.m.

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

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 wrote:

...

Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}import Language.Haskell.TH.Syntaximport Language.Haskell.THimport Language.Haskell.TH.Lift () valueFine :: String -> BoolvalueFine = not . null checkGrammar_2 :: Name -> ExpQcheckGrammar_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 fineCallStack (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 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 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 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 =

...
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)

rulesMap}) 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.

Christopher Done

12:49 p.m.

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

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 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 wrote:

...
Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}import Language.Haskell.TH.Syntaximport Language.Haskell.THimport Language.Haskell.TH.Lift () valueFine :: String -> BoolvalueFine = not . null checkGrammar_2 :: Name -> ExpQcheckGrammar_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 fineCallStack (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 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 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 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 =

...
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)

rulesMap}) 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.

Michael Sloan

1:10 p.m.

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

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 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 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 wrote:

...
Hurray! It works!

{-# LANGUAGE TemplateHaskell #-}import Language.Haskell.TH.Syntaximport Language.Haskell.THimport Language.Haskell.TH.Lift () valueFine :: String -> BoolvalueFine = not . null checkGrammar_2 :: Name -> ExpQcheckGrammar_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 fineCallStack (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 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 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 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 =

...
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)

rulesMap}) 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.

2098

Age (days ago)

2100

Last active (days ago)

List overview

Download

6 comments

2 participants

participants (2)

Christopher Done
Michael Sloan