# Can you automatically generate a parser for a type using type theory some how?

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?

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

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.