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?

  • 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$ – danportin Jul 20 '18 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 Pollard Jul 20 '18 at 18:28
  • $\begingroup$ Google the tool Ott! $\endgroup$ – xuq01 Jul 21 '18 at 7:47
  • $\begingroup$ @LancePollard the latter. It would be nice, since parsing sucks as a task $\endgroup$ – StudySmarterNotHarder Jul 21 '18 at 16:50

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.


Your Answer

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

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