0
$\begingroup$

Was wondering since all the types are spelled out constructively, and the constructions can all be reflected symbolically on a computer, if you can automatically parse expressions in a type?

$\endgroup$
4
  • 1
    $\begingroup$ I'm not sure whether this answers your question, but most presentations of type theories include a grammar for types, which can be translated into a parser generator. For examples, you might look at the parsers for dependently typed languages such as Agda or Gallina (Coq). $\endgroup$
    – emi
    Jul 20, 2018 at 4:13
  • 1
    $\begingroup$ If you wouldn't mind explaining a bit more what you mean that would be helpful. I kind of see what you're getting at but not sure if you mean parsing the type expressions found in math papers, or somehow in a programming language parsing an expression into a type, or something like that. $\endgroup$
    – Lance
    Jul 20, 2018 at 18:28
  • $\begingroup$ Google the tool Ott! $\endgroup$
    – xuq01
    Jul 21, 2018 at 7:47
  • $\begingroup$ @LancePollard the latter. It would be nice, since parsing sucks as a task $\endgroup$ Jul 21, 2018 at 16:50

1 Answer 1

2
$\begingroup$

In programming languages, we usually distinguish concrete syntax, where a program is represented as a linear list of symbols, from abstract syntax, where programs have a tree structure.

The vast majority of PL theory, including most type systems, happens after parsing, working with abstract syntax.

So, it's impossible to generate a parser simply from type rules or definitions, because there are arbitrarily many concrete syntaxes that could correspond to any abstract syntax. The choice is a purely human one.

In some languages, like Haskell, the description of a data type can be used to generate parsers and printers for types, using the deriving mechanism of the typeclass system. But it chooses a syntax that corresponds to the Haskell one by convention, and they could have chosen to define it any other way.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.