0
$\begingroup$

Consider the language of simple types

$$ T \mapsto B \ \mid\ T \rightarrow T \\ B \mapsto \text{Bool} \ \mid\ \text{Int} $$

where $\mapsto$ stands for productions to avoid ambiguity with the terminal "$\rightarrow$" from the language.

If we were to parse this using these combinators, in semi-pseudo-Haskell with hopefully reasonable and obvious naming:

parseTy :: Parser Ty
parseTy = TyArrow <$> parseArrow
      <|> parens parseTy
      <|> TyBase <$> parseBaseTy

parseArrow :: Parser ArrowTy
parseArrow = do
  domTy <- parseTy
  string "->"
  codTy <- parseTy
  pure ArrowTy { .. }

then we'd have infinite recursion through the recursive chain parseTy $\rightarrow$ parseArrow $\rightarrow$ parseTy. The usual solution is, of course, left-factoring this grammar.

But I was lazy to do left factoring, so the following idea occurred to me. Let's say Parser allows us to record the position in the input stream, so what if we record the current position in parseArrow and compare it against the previous one (if any), failing instantly if the position is the same? Or, in code (again pardon my Haskell): we assume some

data ParseState = ParseState
  { lastArrowPos :: Maybe SourcePos
  , ...
  }

and rewrite the combinator for parseArrow as

parseArrow :: Parser ArrowTy
parseArrow = do
  -- get the current position in the stream:
  curPos <- getSourcePos   
  -- get the previous position from the state:
  prevPos <- gets lastArrowPos
  -- fail if they are equal, proceed otherwise:
  guard $ Just curPos /= prevPos

  -- update the state with the new current position:
  modify' $ \st -> st { lastArrowPos = Just curPos }

  -- the rest as before:
  domTy <- parseTy
  string "->"
  codTy <- parseTy
  pure ArrowTy { .. }

This passes all of the tests I've thrown at it (although I haven't formally proven this is a correct approach).

And, to generalize, if we had more than one recursive chain, we'd just have separate SourcePoses in the ParseState.

My primary concern is how it plays with backtracking: what if the combinator is used in a backtracking context, so it seems like it progresses, but then it has to fall back to some previously encountered position? But I wasn't able to neither prove it never happens nor to build a counterexample, nor to find a feasible modification of my method just in case it happens.

So, I have a few questions: is it a well-known approach? If not, are there any issues with it immediately visible? Is it worth it pursuing and formalizing this?

| cite | improve this question | | | | |
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.