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?
0
$\begingroup$
$\endgroup$
-
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$ – portin.daniel 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$ – BananaCats Category Theory App Jul 21 '18 at 16:50
2
$\begingroup$
$\endgroup$
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.
