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