Parsing forall types - should binders be strings or types?
Opened this issue · 0 comments
At the moment, binders in a forall type are represented as Located Type
s. This may not be ideal though.
https://github.com/nihil-lang/nsc/blob/75be47d4271ad74fc440afa3667e3e002e43c90b/lib/nsc-core/src/Language/NStar/Syntax/Core.hs#L68-L71
One thing it forces us, is to put error
s (or functions which do the same) on normally unreachable pattern.
For example, let's say we'd want to get all the variable names bound by a forall
. We would need to write this:
keys [] = []
keys ((Var v :@ _, _) : xs) = v : keys xs
keys ((t :@ _, _) : _) = error ("Trying to get name of non-type variable '" <> show t <> "'")
But the last case should not really be here. In fact, we are guaranteed to have Var
s thanks to the parser
https://github.com/nihil-lang/nsc/blob/75be47d4271ad74fc440afa3667e3e002e43c90b/lib/nsc-parser/src/Language/NStar/Syntax/Parser.hs#L169-L177
But removing the last case leads us to a GHC warning on incomplete pattern matching, which we would really want to not have at all, while not having to put an error
-alike function as a placeholder, though it might not be the worst idea (instead of putting something like []
or mempty
, which won't tell there is something going on that should not be going on).
But having binders be represented by their names gets rid of this mess, while probably maintaining good and readable code.
I just don't know whether I should stick to Type
s or not.