Lander Lopez- What FP Can Learn From Formal Languages: Towards a Leaner Syntax- λC 2019
We love pure FP. However, due to the syntactic overhead, types “get in the way.” Looking for a leaner syntax, we’ll seek inspiration in formal language theory. We’ll discover striking similarities with advanced FP type systems and explore whether we can do pure FP with a “dynamic feel.” In pure FP, we create descriptions of programs, abstracting from the computation and operational concerns. Analogously, domain-specific languages are interpreted into a target language or computation. However, statically-typed FP languages carry a syntactic overhead hampering the expressivity and fluency required for ergonomic DSLs. In this talk, I will argue that much of this syntactic overhead is accidental. The goal is that our libraries and APIs look like mini DSLs without compromising what we love in modern pure FP: HKTs, parametricity, effects as values, etc. Types should not get in the way. We will seek inspiration from the natural language experts, the formal grammar and NLP fields. There is an obvious connection between formal grammars and PLT as they are the foundation for compiler design and parsing in general. This talk will look into a deeper connection, arising from seeing type systems also as a “grammar” for all their possible inhabitants. Then the composition of those values will provide the valid “sentences” in our program. It doesn’t come as a surprise that concepts like parametricity have been developed independently in both the formal grammar and PLT camps. Also, for a long time, example texts could be generated from grammars. Similarly, now the FP practitioner can also generate random valid examples from types to enable property-based testing. Looking further, we can wonder if type definitions will be derived from examples the way grammars can be inferred from example texts. After presenting the similarities, we will look into three fundamental properties of formal languages that I would like to see fully embraced in pure FP languages: * Structurality. Language grammars are fully structural while PLTs add nominality to the mix. Grammars allow structure to be enclosed into other structures recursively. In PLTs we have HKTs to stack structure, an additional machinery that, in general, does not abstract over kinds. * Algebraic nature. At the data level, we have algebraic data types, but algebraic composition doesn’t extend to functions and application. In grammars, the composition and extension of rules and reductions are purely algebraic. We’ll explore how algebraic function application and composition could make for a leaner syntax and simpler machinery for threading errors and effects. * First class terminal objects. In formal languages, the terminal objects and the production rules are both first class, while type systems have the value vs. type divide. Fortunately, dependently-typed languages are blurring the distinction and values can be used at the type level definition. We will present how these properties could reduce syntactic overhead while increasing expressivity and enabling the definition of fluent DSLs and APIs. The talk will require basic familiarity with higher kinded, pure FP type systems at a practitioner level. No theoretical background will be necessary. The content will include many graph-based representations and code examples in Haskell and Scala. An exploration of how we can evolve current FP language syntax to have the “dynamic typing” feel without compromising on types.
We love pure FP. However, due to the syntactic overhead, types “get in the way.” Looking for a leaner syntax, we’ll seek inspiration in formal language theory. We’ll discover striking similarities with advanced FP type systems and explore whether we can do pure FP with a “dynamic feel.” In pure FP, we create descriptions of programs, abstracting from the computation and operational concerns. Analogously, domain-specific languages are interpreted into a target language or computation. However, statically-typed FP languages carry a syntactic overhead hampering the expressivity and fluency required for ergonomic DSLs. In this talk, I will argue that much of this syntactic overhead is accidental. The goal is that our libraries and APIs look like mini DSLs without compromising what we love in modern pure FP: HKTs, parametricity, effects as values, etc. Types should not get in the way. We will seek inspiration from the natural language experts, the formal grammar and NLP fields. There is an obvious connection between formal grammars and PLT as they are the foundation for compiler design and parsing in general. This talk will look into a deeper connection, arising from seeing type systems also as a “grammar” for all their possible inhabitants. Then the composition of those values will provide the valid “sentences” in our program. It doesn’t come as a surprise that concepts like parametricity have been developed independently in both the formal grammar and PLT camps. Also, for a long time, example texts could be generated from grammars. Similarly, now the FP practitioner can also generate random valid examples from types to enable property-based testing. Looking further, we can wonder if type definitions will be derived from examples the way grammars can be inferred from example texts. After presenting the similarities, we will look into three fundamental properties of formal languages that I would like to see fully embraced in pure FP languages: * Structurality. Language grammars are fully structural while PLTs add nominality to the mix. Grammars allow structure to be enclosed into other structures recursively. In PLTs we have HKTs to stack structure, an additional machinery that, in general, does not abstract over kinds. * Algebraic nature. At the data level, we have algebraic data types, but algebraic composition doesn’t extend to functions and application. In grammars, the composition and extension of rules and reductions are purely algebraic. We’ll explore how algebraic function application and composition could make for a leaner syntax and simpler machinery for threading errors and effects. * First class terminal objects. In formal languages, the terminal objects and the production rules are both first class, while type systems have the value vs. type divide. Fortunately, dependently-typed languages are blurring the distinction and values can be used at the type level definition. We will present how these properties could reduce syntactic overhead while increasing expressivity and enabling the definition of fluent DSLs and APIs. The talk will require basic familiarity with higher kinded, pure FP type systems at a practitioner level. No theoretical background will be necessary. The content will include many graph-based representations and code examples in Haskell and Scala. An exploration of how we can evolve current FP language syntax to have the “dynamic typing” feel without compromising on types.