Hello Greg,It seems that I am late for the party but we used a GADT parser in the tool we built for our Generating Generic Functions paper[1]. It so happens that I made slides for this material so, if you're interested you can have a look at [2].
The motivation for doing this was that we needed to
On Oct 31, 2006, at 2:19 AM, Dimitrios Vytiniotis wrote:
-- Give a GADT for representation types
data R a where
Rint :: R Int
Rbool :: R Bool
Rpair :: R a - R b - R (a,b)
-- Give an existential type with a type representation
data TermEx where
MkTerm :: R a - Term a - TermEx
-- we
Thanks to everyone who replied (especially Dimitrios Vytiniotis and
Joost Visser). I now know the standard way to write the GADT parser.
But I'm still curious if anyone has comments pertaining to the version
using type classes. It seems so close to doing what we want, and it is
pretty
I'm trying to create a simple parser for the GADT evaluator from the
wobbly types paper, and I need a little help. Here's the GADT and the
evaluator...
data Term a where
Lit :: Int - Term Int
Inc :: Term Int - Term Int
IsZ :: Term Int - Term Bool
If :: Term Bool -
I don't have an answer, but would be extremely interested in knowing
one!
one of my first attempts to use GADTs was to do something similar,
implemening the simple polymorphic lambda calculus in a way that
transformations could be guarenteed typesafe statically, but then when I
went and tried to
Hi Greg,
We've built some GADT parsers recently to fit our two-level
transformation library with front-ends for for XML Schema and SQL.
See Coupled Schema Transformation and Data Conversion For XML and
SQL (PADL 2007) if you're interested. The trick is to use a
constructor in which the a
Just noticed Joost Visser's message but since I
had (essentially a very similar) response I thought I might
send it off as well ... It includes the conditional cases.
Regards,
-d
{-# OPTIONS_GHC -fglasgow-exts #-}
module Main where
data Term a where
Lit :: Int - Term Int
Inc ::
