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
- Add image to JCheckBoxMenuItem
- How to access invisible Unordered List element with Selenium WebDriver using Java
- Inheritance in Java, apparent type vs actual type
- Java catch the ball Game
- Access objects variable & method by name
- GridBagLayout is displaying JTextField and JTextArea as short, vertical lines
- Perform a task each interval
- Compound classes stored in an array are not accessible in selenium java
- How to avoid concurrent access to a resource?
- Why does processing goes slower on implementing try catch block in java?
Related Questions in PROGRAMMING-LANGUAGES
- Add image to JCheckBoxMenuItem
- How to access invisible Unordered List element with Selenium WebDriver using Java
- Inheritance in Java, apparent type vs actual type
- Java catch the ball Game
- Access objects variable & method by name
- GridBagLayout is displaying JTextField and JTextArea as short, vertical lines
- Perform a task each interval
- Compound classes stored in an array are not accessible in selenium java
- How to avoid concurrent access to a resource?
- Why does processing goes slower on implementing try catch block in java?
Related Questions in FORMAL-LANGUAGES
- Add image to JCheckBoxMenuItem
- How to access invisible Unordered List element with Selenium WebDriver using Java
- Inheritance in Java, apparent type vs actual type
- Java catch the ball Game
- Access objects variable & method by name
- GridBagLayout is displaying JTextField and JTextArea as short, vertical lines
- Perform a task each interval
- Compound classes stored in an array are not accessible in selenium java
- How to avoid concurrent access to a resource?
- Why does processing goes slower on implementing try catch block in java?
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.