🔥 Naming, Name, & Gensym #202
Conversation
| ) | ||
| => Analysis address value m | ||
| -> (Term Core User -> m value) | ||
| -> (Term Core User -> m value) |
There was a problem hiding this comment.
eval now expects User names.
| Lam _ b -> do | ||
| n <- Gen <$> fresh | ||
| abstract eval n (instantiate (const (pure n)) b) | ||
| Lam (Ignored n) b -> abstract eval n (instantiate1 (pure n) b) |
There was a problem hiding this comment.
Instead of generating a fresh name and substituting it in, we instantiate the scope with the name the user gave the variable. Note that this is probably not what we’re going to want to do for e.g. computed functions, but since we evaluate by analysis instead of by substitution it should be safe.
patrickt
left a comment
patrickt
left a comment
There was a problem hiding this comment.
Other than the question about User versus Name (and that’s not hugely important to me; I’d prefer to go with the established conventions in the literature), this looks 💯.
| Lam _ b -> do | ||
| n <- Gen <$> fresh | ||
| abstract eval n (instantiate (const (pure n)) b) | ||
| Lam (Ignored n) b -> abstract eval n (instantiate1 (pure n) b) |
| [ let' "x" .= pure "_x" | ||
| , let' "y" .= pure "_y"])) | ||
| [ let' "this" .= Core.frame | ||
| , pure "this" Core.... let' "x" .= pure "_x" |
There was a problem hiding this comment.
$DEITY bless the Haskell parser for gamely accepting Core.....
There was a problem hiding this comment.
Core.... I haven’t heard that name in years....
| import Data.Text.Prettyprint.Doc (Pretty (..)) | ||
|
|
||
| -- | User-specified and -relevant names. | ||
| type User = Text |
There was a problem hiding this comment.
At this point, now that there aren’t different varieties of names between which we have to distinguish, are we better off calling this Name, if only for the immediate comprehension of people new to the codebase?
There was a problem hiding this comment.
Going to do this in a later PR to avoid conflicts.
This PR simplifies our treatment of names significantly, 🔥ing
Naming,Name, andGensymin favour of much simpler local instantiations and folds.