Re: [GHC] #8920: Alternative GADT syntax

22 Mar 2014


      #8920: Alternative GADT syntax
-------------------------------------+-------------------------------------
        Reporter:  guest             |            Owner:
            Type:  feature request   |           Status:  new
        Priority:  normal            |        Milestone:  7.10.1
       Component:  Compiler          |          Version:  7.8.1-rc2
  (Parser)                           |         Keywords:  gadts
      Resolution:                    |     Architecture:  Unknown/Multiple
Operating System:  Unknown/Multiple  |       Difficulty:  Moderate (less
 Type of failure:  Other             |  than a day)
       Test Case:                    |       Blocked By:
        Blocking:                    |  Related Tickets:
-------------------------------------+-------------------------------------
Description changed by simonpj:

Old description:
...
An alternative syntax for GADTs
Instead of
{{{
data Term x where
    K :: Term (a -> b -> a)
    S :: Term ((a -> b -> c)  -> (a -> b) -> a -> c)
    Const :: a -> Term a
    (:@) :: Term (a -> b) -> (Term a) -> Term b
}}}
You can write
{{{
data Term x = K :: Term (a -> b -> a) | S :: Term ((a -> b -> c)  -> (a
-> b) -> a -> c) | Const a :: Term a | (:@) (Term (a -> b)) (Term a) ::
Term b
}}}
New description:

 An alternative syntax for GADTs

 Instead of
 {{{
 data Term x where
     K :: Term (a -> b -> a)
     S :: Term ((a -> b -> c)  -> (a -> b) -> a -> c)
     Const :: a -> Term a
     (:@) :: Term (a -> b) -> (Term a) -> Term b
 }}}

 You can write
 {{{
 data Term x = K :: Term (a -> b -> a)
             | S :: Term ((a -> b -> c)  -> (a -> b) -> a -> c)
             | Const a :: Term a
             | (:@) (Term (a -> b)) (Term a) :: Term b
 }}}

--

--
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/8920#comment:1
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler