Ticket #7915: 0001-Documentation-use-new-syntax-for-record-GADTs-7915.patch

File 0001-Documentation-use-new-syntax-for-record-GADTs-7915.patch, 2.5 KB (added by monoidal, 2 years ago)
  • docs/users_guide/glasgow_exts.xml

    From dfb8dadc8066340cbdc2905a5ec78834e0571304 Mon Sep 17 00:00:00 2001
    From: Krzysztof Gogolewski <[email protected]>
    Date: Thu, 16 May 2013 15:54:59 +0200
    Subject: [PATCH] Documentation: use new syntax for record GADTs (#7915)
    
    ---
     docs/users_guide/glasgow_exts.xml | 33 ++++++++++++++++-----------------
     1 file changed, 16 insertions(+), 17 deletions(-)
    
    diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
    index 3407de5..c97489b 100644
    a b selectors. 
    30713071Here is the example of that section, in GADT-style syntax:
    30723072<programlisting>
    30733073data Counter a where
    3074     NewCounter { _this    :: self
    3075                , _inc     :: self -> self
    3076                , _display :: self -> IO ()
    3077                , tag      :: a
    3078                }
    3079         :: Counter a
     3074    NewCounter :: { _this    :: self
     3075                  , _inc     :: self -> self
     3076                  , _display :: self -> IO ()
     3077                  , tag      :: a
     3078                  } -> Counter a
    30803079</programlisting>
    30813080As before, only one selector function is generated here, that for <literal>tag</literal>.
    30823081Nevertheless, you can still use all the field names in pattern matching and record construction.
    As mentioned in <xref linkend="gadt-style"/>, record syntax is supported. 
    31883187For example:
    31893188<programlisting>
    31903189  data Term a where
    3191       Lit    { val  :: Int }      :: Term Int
    3192       Succ   { num  :: Term Int } :: Term Int
    3193       Pred   { num  :: Term Int } :: Term Int
    3194       IsZero { arg  :: Term Int } :: Term Bool
    3195       Pair   { arg1 :: Term a
    3196              , arg2 :: Term b
    3197              }                    :: Term (a,b)
    3198       If     { cnd  :: Term Bool
    3199              , tru  :: Term a
    3200              , fls  :: Term a
    3201              }                    :: Term a
     3190      Lit    :: { val  :: Int }      -> Term Int
     3191      Succ   :: { num  :: Term Int } -> Term Int
     3192      Pred   :: { num  :: Term Int } -> Term Int
     3193      IsZero :: { arg  :: Term Int } -> Term Bool
     3194      Pair   :: { arg1 :: Term a
     3195                , arg2 :: Term b
     3196                }                    -> Term (a,b)
     3197      If     :: { cnd  :: Term Bool
     3198                , tru  :: Term a
     3199                , fls  :: Term a
     3200                }                    -> Term a
    32023201</programlisting>
    32033202However, for GADTs there is the following additional constraint:
    32043203every constructor that has a field <literal>f</literal> must have