[[project @ 2005-11-28 09:40:19 by simonpj]
simonpj**20051128094019
Document record syntax for GADTs and existentials (thanks Autrijus)
] {
hunk ./ghc/docs/users_guide/glasgow_exts.xml 1212
-An easy extension (implemented in hbc) is to allow
+An easy extension is to allow
hunk ./ghc/docs/users_guide/glasgow_exts.xml 1270
+
+Record Constructors
+
+
+GHC allows existentials to be used with records syntax as well. For example:
+
+
+data Counter a = forall self. NewCounter
+ { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+
+Here tag is a public field, with a well-typed selector
+function tag :: Counter a -> a. The self
+type is hidden from the outside; any attempt to apply _this,
+_inc or _output as functions will raise a
+compile-time error. In other words, GHC defines a record selector function
+only for fields whose type does not mention the existentially-quantified variables.
+(This example used an underscore in the fields for which record selectors
+will not be defined, but that is only programming style; GHC ignores them.)
+
+
+
+To make use of these hidden fields, we need to create some helper functions:
+
+
+inc :: Counter a -> Counter a
+inc (NewCounter x i d t) = NewCounter
+ { _this = i x, _inc = i, _display = d, tag = t }
+
+display :: Counter a -> IO ()
+display NewCounter{ _this = x, _display = d } = d x
+
+
+Now we can define counters with different underlying implementations:
+
+
+counterA :: Counter String
+counterA = NewCounter
+ { _this = 0, _inc = (1+), _display = print, tag = "A" }
+
+counterB :: Counter String
+counterB = NewCounter
+ { _this = "", _inc = ('#':), _display = putStrLn, tag = "B" }
+
+main = do
+ display (inc counterA) -- prints "1"
+ display (inc (inc counterB)) -- prints "##"
+
+
+In GADT declarations (see ), the explicit
+forall may be omitted. For example, we can express
+the same Counter a using GADT:
+
+
+data Counter a where
+ NewCounter { _this :: self
+ , _inc :: self -> self
+ , _display :: self -> IO ()
+ , tag :: a
+ }
+ :: Counter a
+
+
+At the moment, record update syntax is only supported for Haskell 98 data types,
+so the following function does not work:
+
+
+-- This is invalid; use explicit NewCounter instead for now
+setTag :: Counter a -> a -> Counter a
+setTag obj t = obj{ tag = t }
+
+
+
+
+
+
+
hunk ./ghc/docs/users_guide/glasgow_exts.xml 3629
- eval (IsZero i) = eval i == 0
+ eval (IsZero t) = eval t == 0
hunk ./ghc/docs/users_guide/glasgow_exts.xml 3631
- eval (Pair e1 e2) = (eval e2, eval e2)
+ eval (Pair e1 e2) = (eval e1, eval e2)
hunk ./ghc/docs/users_guide/glasgow_exts.xml 3663
-You cannot use record syntax on a GADT-style data type declaration. (
-It's not clear what these it would mean. For example,
-the record selectors might ill-typed.)
-However, you can use strictness annotations, in the obvious places
+You can use record syntax on a GADT-style data type declaration:
+
+
+ data Term a where
+ Lit { val :: Int } :: Term Int
+ Succ { num :: Term Int } :: Term Int
+ Pred { num :: Term Int } :: Term Int
+ IsZero { arg :: Term Int } :: Term Bool
+ Pair { arg1 :: Term a
+ , arg2 :: Term b
+ } :: Term (a,b)
+ If { cnd :: Term Bool
+ , tru :: Term a
+ , fls :: Term a
+ } :: Term a
+
+For every constructor that has a field f, (a) the type of
+field f must be the same; and (b) the
+result type of the constructor must be the same; both modulo alpha conversion.
+Hence, in our example, we cannot merge the num and arg
+fields above into a
+single name. Although their field types are both Term Int,
+their selector functions actually have different types:
+
+
+ num :: Term Int -> Term Int
+ arg :: Term Bool -> Term Int
+
+
+At the moment, record updates are not yet possible with GADT, so support is
+limited to record construction, selection and pattern matching:
+
+
+ someTerm :: Term Bool
+ someTerm = IsZero { arg = Succ { num = Lit { val = 0 } } }
+
+ eval :: Term a -> a
+ eval Lit { val = i } = i
+ eval Succ { num = t } = eval t + 1
+ eval Pred { num = t } = eval t - 1
+ eval IsZero { arg = t } = eval t == 0
+ eval Pair { arg1 = t1, arg2 = t2 } = (eval t1, eval t2)
+ eval t@If{} = if eval (cnd t) then eval (tru t) else eval (fls t)
+
+
+
+
+
+You can use strictness annotations, in the obvious places
}