The syntax for algebraic data types is very similar to the syntax of Backus–Naur Form, which is used to describe context-free grammars. That got me thinking, if we think of the Haskell type checker as a parser for a language, represented as an algebraic data type (nularry type constructors representing the terminal symbols, for example), is the set of all languages accepted the same as the set of context free languages? Also, with this interpretation, what set of formal languages can GADTs accept?
Are regular haskell algebraic data types equivalent to context free grammars? What about GADTS?
1.2k views Asked by Nathan BeDell At
1
There are 1 answers
Related Questions in HASKELL
- How to not load all database records in my TListbox in Firemonkey Delphi XE8
- How to catch WM_DEVICECHANGE in a control other than TForm?
- show information with Rolling / moving messages delphi xe7
- What is the different between "Console target" and "GUI target" in DCC32 option?
- How to add new online ressources to RAD Studio help system
- C# and Delphi code have different behaviour when importing unmanaged dll
- Loop through records on a cxgrid and update a field/column
- Delphi 7 - Save to a Specific .INI Files Name
- TImagelist for large images
- how to modify a function so it returns an array of strings
Related Questions in PROGRAMMING-LANGUAGES
- How to not load all database records in my TListbox in Firemonkey Delphi XE8
- How to catch WM_DEVICECHANGE in a control other than TForm?
- show information with Rolling / moving messages delphi xe7
- What is the different between "Console target" and "GUI target" in DCC32 option?
- How to add new online ressources to RAD Studio help system
- C# and Delphi code have different behaviour when importing unmanaged dll
- Loop through records on a cxgrid and update a field/column
- Delphi 7 - Save to a Specific .INI Files Name
- TImagelist for large images
- how to modify a function so it returns an array of strings
Related Questions in FORMAL-LANGUAGES
- How to not load all database records in my TListbox in Firemonkey Delphi XE8
- How to catch WM_DEVICECHANGE in a control other than TForm?
- show information with Rolling / moving messages delphi xe7
- What is the different between "Console target" and "GUI target" in DCC32 option?
- How to add new online ressources to RAD Studio help system
- C# and Delphi code have different behaviour when importing unmanaged dll
- Loop through records on a cxgrid and update a field/column
- Delphi 7 - Save to a Specific .INI Files Name
- TImagelist for large images
- how to modify a function so it returns an array of strings
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Popular Tags
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
First of all, data types do not always describe a set of strings (i.e., a language). That is, while a list type does, a tree type does not. One might counter that we could "flatten" the trees into lists and think of that as their language. Yet, what about data types like
or, worse
?
Polynomial types (types without
->
inside) roughly describe trees, which can be flattened (in-order visited), so let's use those as an example.As you have observed, writing a CFG as a (polynomial) type is easy, since you can exploit recursion
above
A
expresses{ Int^m Char^n | m>n }
.GADTs go much beyond context-free languages.
above
ABC
expresses the (flattened) languageA^n B^n C^n
, which is not context-free.You are pretty much unrestricted with GADTs, since it's easy to encode arithmetics with them. That is you can build a type
Plus a b c
which is non-empty iffc=a+b
with Peano naturals. You can also build a typeHalt n m
which is non-empty iff the Turing machinem
halts on inputm
. So, you can build a languagewhich is recursive (and not in any simpler class, roughly).
At the moment, I do not know whether you can describe recursively enumerable (computably enumerable) languages in GADTs. Even in the halting problem example, I have to include the "proof" term inside the GADT to make it work.
Intuitively, if you have a string of length
n
and you want to check it a against a GADT, you can build all the GADT terms of depthn
, flatten them, and then compare to the string. This should prove that such language is always recursive. However, existential types make this tree building approach quite tricky, so I do not have a definite answer right now.