8ea902d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added %hide and %freeze directives

commit8ea902df4a0b9570f5d9cda4acba9954275267e8 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateTue 27 Dec 2011, 20:59 (15 years ago) parentdd03041

12 files changed+171−43

compare with master

unifiedsplit

impl-paper/macros.ltx+3−3 impl-paper/syntax.tex+10−1 impl-paper/typechecking.tex+17 lib/prelude/list.idr+4 lib/prelude/strings.idr+11 src/Core/Evaluate.hs+49−26 src/Core/TT.hs+8−3 src/Idris/AbsSyntax.hs+13−1 src/Idris/ElabTerm.hs+1−1 src/Idris/IBC.hs+29−6 src/Idris/Parser.hs+6 tutorial/typesfuns.tex+20−2

impl-paper/macros.ltx+3−3

@@ -387,7 +387,7 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

387387

388388%%%%%%%%%%%% TYPE

389389

390−\newcommand{\Type}{\mbox{\texttt{\#}}} %\star}

390+\newcommand{\Type}{\mbox{\texttt{Set}}} %\star}

391391

392392

393393%%%%%%%%%%%%% ARROWS

@@ -600,8 +600,8 @@ Program & Version & Instructions & Thunks & Memory Accesses & Cells \\

600600\newcommand{\farrow}{\Rightarrow}

601601\newcommand{\lookup}{\FN{lookup}}

602602

603−% \newcommand{\source}{\Lang{TT}}

604−\newcommand{\source}{\textbf{DT-Res}}

603+\newcommand{\source}{\Lang{TT}}

604+%\newcommand{\source}{\textbf{DT-Res}}

605605\newcommand{\target}{\Lang{ExTT}}

606606\newcommand{\runtime}{\Lang{RunTT}}

607607

impl-paper/syntax.tex+10−1

@@ -1 +1,10 @@

1−\section{Syntactic Sugar}

1+\section{High Level Structures}

3+\subsection{\texttt{where} clauses}

5+\subsection{The \texttt{with} rule}

7+\subsection{Type Classes}

9+\subsection{Syntactic Sugar}

10+

impl-paper/typechecking.tex+17

@@ -1 +1,18 @@

11\section{The Core Type Theory}

3+\DM{

4+\begin{array}{rll@{\hg}|rll}

5+\vt ::= & \Type_i & (\mbox{type universes}) &

6+\hg\vb ::= & \lam{\vx}{\vt} & (\mbox{abstraction}) \\

8+ \mid & \vx & (\mbox{variable}) &

9+ \mid & \LET\:\vx\defq\vt\Hab\vt & (\mbox{let binding}) \\

10+

11+ \mid & \vb\SC\:\vt & (\mbox{binding}) &

12+ \mid & \all{\vx}{\vt} & (\mbox{function space}) \\

13+

14+ \mid & \vt\:\vt & (\mbox{application})

15+

16+\end{array}

17+}

18+

lib/prelude/list.idr+4

@@ -50,6 +50,10 @@ elem : Eq a => a -> List a -> Bool;

5050elem x [] = False;

5151elem x (y :: ys) = if (x == y) then True else (elem x ys);

5252

53+lookup : Eq k => k -> List (k, v) -> Maybe v;

54+lookup k [] = Nothing;

55+lookup k ((x, v) :: xs) = if (x == k) then (Just v) else (lookup k xs);

56+

5357sort : Ord a => List a -> List a;

5458sort [] = [];

5559sort [x] = [x];

lib/prelude/strings.idr+11

@@ -2,6 +2,7 @@ module prelude.strings;

33import builtins;

44import prelude.list;

5+import prelude.char;

67-- Some more complex string operations

@@ -49,3 +50,13 @@ break p = span (not . p);

4950

5051split : (Char -> Bool) -> String -> List String;

5152split p xs = map pack (split p (unpack xs));

53+

54+ltrim : String -> String;

55+ltrim xs with strM xs {

56+ ltrim "" | StrNil = "";

57+ ltrim (strCons x xs) | StrCons _ _

58+ = if (isSpace x) then (ltrim xs) else (strCons x xs);

59+}

60+

61+trim : String -> String;

62+trim xs = ltrim (rev (ltrim (rev xs)));

src/Core/Evaluate.hs+49−26

@@ -2,9 +2,9 @@

22 PatternGuards #-}

44module Core.Evaluate(normalise, normaliseC, simplify, specialise, hnf,

5− Def(..),

5+ Def(..), Accessibility(..),

66 Context, initContext, ctxtAlist, uconstraints, next_tvar,

7− addToCtxt, addCtxtDef, addTyDecl, addDatatype,

7+ addToCtxt, setAccess, addCtxtDef, addTyDecl, addDatatype,

88 addCasedef, addOperator,

99 lookupTy, lookupP, lookupDef, lookupVal, lookupTyEnv,

1010 Value(..)) where

@@ -108,11 +108,11 @@ eval ctxt statics genv tm opts = ev True [] tm where

108108

109109 ev top env (P _ n ty)

110110 | Just (Let t v) <- lookup n genv = ev top env v

111− ev top env (P Ref n ty) = case lookupDef Nothing n ctxt of

112− [Function _ tm] -> ev True env tm

113− [TyDecl nt ty] -> do vty <- ev True env ty

114− return $ VP nt n vty

115− [CaseOp inl _ _ [] tree] ->

111+ ev top env (P Ref n ty) = case lookupDefAcc Nothing n ctxt of

112+ [(Function _ tm, Public)] -> trace ("Eval " ++ show n) $ ev True env tm

113+ [(TyDecl nt ty, _)] -> do vty <- ev True env ty

114+ return $ VP nt n vty

115+ [(CaseOp inl _ _ [] tree, Public)] ->

116116 if simpl && (not inl)

117117 then liftM (VP Ref n) (ev top env ty)

118118 else do c <- evCase top env [] [] tree

@@ -153,7 +153,7 @@ eval ctxt statics genv tm opts = ev True [] tm where

153153 apply False env f args

154154 | spec = return $ unload env f args

155155 apply top env (VP Ref n ty) args

156− | [CaseOp inl _ _ ns tree] <- lookupDef Nothing n ctxt

156+ | [(CaseOp inl _ _ ns tree, Public)] <- lookupDefAcc Nothing n ctxt

157157 = -- traceWhen (n == UN ["interp"]) (show (n, args)) $

158158 if simpl && (not inl) then return $ unload env (VP Ref n ty) args

159159 else do c <- evCase top env ns args tree

@@ -449,32 +449,47 @@ instance Binary (a -> b) where

449449

450450-------

451451

452+-- Frozen => doesn't reduce

453+-- Hidden => doesn't reduce and invisible to type checker

454+

455+data Accessibility = Public | Frozen | Hidden

456+ deriving (Show, Eq)

457+{-!

458+deriving instance Binary Accessibility

459+!-}

460+

452461data Context = MkContext { uconstraints :: [UConstraint],

453462 next_tvar :: Int,

454− definitions :: Ctxt Def }

463+ definitions :: Ctxt (Def, Accessibility) }

455464

456465initContext = MkContext [] 0 emptyContext

457466

458467ctxtAlist :: Context -> [(Name, Def)]

459−ctxtAlist ctxt = toAlist (definitions ctxt)

468+ctxtAlist ctxt = map (\(n, (d, a)) -> (n, d)) $ toAlist (definitions ctxt)

460469

461470veval ctxt env t = evalState (eval ctxt emptyContext env t []) ()

462471

463472addToCtxt :: Name -> Term -> Type -> Context -> Context

464473addToCtxt n tm ty uctxt

465474 = let ctxt = definitions uctxt

466− ctxt' = addDef n (Function ty tm) ctxt in

475+ ctxt' = addDef n (Function ty tm, Public) ctxt in

467476 uctxt { definitions = ctxt' }

468477

478+setAccess :: Name -> Accessibility -> Context -> Context

479+setAccess n a uctxt

480+ = let ctxt = definitions uctxt

481+ ctxt' = updateDef n (\ (d, _) -> (d, a)) ctxt in

482+ uctxt { definitions = ctxt' }

483+

469484addCtxtDef :: Name -> Def -> Context -> Context

470485addCtxtDef n d c = let ctxt = definitions c

471− ctxt' = addDef n d ctxt in

486+ ctxt' = addDef n (d, Public) ctxt in

472487 c { definitions = ctxt' }

473488

474489addTyDecl :: Name -> Type -> Context -> Context

475490addTyDecl n ty uctxt

476491 = let ctxt = definitions uctxt

477− ctxt' = addDef n (TyDecl Ref ty) ctxt in

492+ ctxt' = addDef n (TyDecl Ref ty, Public) ctxt in

478493 uctxt { definitions = ctxt' }

479494

480495addDatatype :: Datatype Name -> Context -> Context

@@ -482,14 +497,14 @@ addDatatype (Data n tag ty cons) uctxt

482497 = let ctxt = definitions uctxt

483498 ty' = normalise uctxt [] ty

484499 ctxt' = addCons 0 cons (addDef n

485− (TyDecl (TCon tag (arity ty')) ty) ctxt) in

500+ (TyDecl (TCon tag (arity ty')) ty, Public) ctxt) in

486501 uctxt { definitions = ctxt' }

487502 where

488503 addCons tag [] ctxt = ctxt

489504 addCons tag ((n, ty) : cons) ctxt

490505 = let ty' = normalise uctxt [] ty in

491506 addCons (tag+1) cons (addDef n

492− (TyDecl (DCon tag (arity ty')) ty) ctxt)

507+ (TyDecl (DCon tag (arity ty')) ty, Public) ctxt)

493508

494509addCasedef :: Name -> Bool -> Bool -> [(Term, Term)] -> Type -> Context -> Context

495510addCasedef n alwaysInline tcase ps ty uctxt

@@ -497,7 +512,8 @@ addCasedef n alwaysInline tcase ps ty uctxt

497512 ps' = ps -- simpl ps in

498513 ctxt' = case simpleCase tcase ps' of

499514 CaseDef args sc -> let inl = alwaysInline in

500− addDef n (CaseOp inl ty ps args sc) ctxt in

515+ addDef n (CaseOp inl ty ps args sc,

516+ Public) ctxt in

501517 uctxt { definitions = ctxt' }

502518 where simpl [] = []

503519 simpl ((l,r) : xs) = (l, simplify uctxt [] r) : simpl xs

@@ -505,13 +521,13 @@ addCasedef n alwaysInline tcase ps ty uctxt

505521addOperator :: Name -> Type -> Int -> ([Value] -> Maybe Value) -> Context -> Context

506522addOperator n ty a op uctxt

507523 = let ctxt = definitions uctxt

508− ctxt' = addDef n (Operator ty a op) ctxt in

524+ ctxt' = addDef n (Operator ty a op, Public) ctxt in

509525 uctxt { definitions = ctxt' }

510526

511527lookupTy :: Maybe [String] -> Name -> Context -> [Type]

512528lookupTy root n ctxt

513529 = do def <- lookupCtxt root n (definitions ctxt)

514− case def of

530+ case fst def of

515531 (Function ty _) -> return ty

516532 (TyDecl _ ty) -> return ty

517533 (Operator ty _ _) -> return ty

@@ -520,20 +536,26 @@ lookupTy root n ctxt

520536lookupP :: Maybe [String] -> Name -> Context -> [Term]

521537lookupP root n ctxt

522538 = do def <- lookupCtxt root n (definitions ctxt)

523− case def of

524− (Function ty tm) -> return (P Ref n ty)

525− (TyDecl nt ty) -> return (P nt n ty)

526− (CaseOp _ ty _ _ _) -> return (P Ref n ty)

527− (Operator ty _ _) -> return (P Ref n ty)

539+ p <- case def of

540+ (Function ty tm, a) -> return (P Ref n ty, a)

541+ (TyDecl nt ty, a) -> return (P nt n ty, a)

542+ (CaseOp _ ty _ _ _, a) -> return (P Ref n ty, a)

543+ (Operator ty _ _, a) -> return (P Ref n ty, a)

544+ case snd p of

545+ Hidden -> []

546+ _ -> return (fst p)

528547

529548lookupDef :: Maybe [String] -> Name -> Context -> [Def]

530−lookupDef root n ctxt = lookupCtxt root n (definitions ctxt)

549+lookupDef root n ctxt = map fst $ lookupCtxt root n (definitions ctxt)

550+

551+lookupDefAcc :: Maybe [String] -> Name -> Context -> [(Def, Accessibility)]

552+lookupDefAcc root n ctxt = lookupCtxt root n (definitions ctxt)

531553

532554lookupVal :: Maybe [String] -> Name -> Context -> [Value]

533555lookupVal root n ctxt

534556 = do def <- lookupCtxt root n (definitions ctxt)

535− case def of

536− (Function _ htm) -> return (veval ctxt [] htm)

557+ case fst def of

558+ (Function _ htm) -> return (veval ctxt [] htm)

537559 (TyDecl nt ty) -> return (VP nt n (veval ctxt [] ty))

538560

539561lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

@@ -542,3 +564,4 @@ lookupTyEnv n env = li n 0 env where

542564 li n i ((x, b): xs)

543565 | n == x = Just (i, binderTy b)

544566 | otherwise = li n (i+1) xs

567+

src/Core/TT.hs+8−3

@@ -110,8 +110,8 @@ instance Show Name where

110110 show (MN i s) = "{" ++ s ++ show i ++ "}"

111111

112112

113−-- Contexts allow us to map names to things

114−-- TODO: Namespaces and ambiguous names

113+-- Contexts allow us to map names to things. A root name maps to a collection

114+-- of things in different namespaces with that name.

115115

116116type Ctxt a = Map.Map Name (Map.Map Name a)

117117emptyContext = Map.empty

@@ -119,7 +119,7 @@ emptyContext = Map.empty

119119nsroot (NS n _) = n

120120nsroot n = n

121121

122−addDef :: Show a => Name -> a -> Ctxt a -> Ctxt a

122+addDef :: Name -> a -> Ctxt a -> Ctxt a

123123addDef n v ctxt = case Map.lookup (nsroot n) ctxt of

124124 Nothing -> Map.insert (nsroot n)

125125 (Map.insert n v Map.empty) ctxt

@@ -155,6 +155,11 @@ lookupCtxtName nspace n ctxt = case Map.lookup (nsroot n) ctxt of

155155lookupCtxt :: Maybe [String] -> Name -> Ctxt a -> [a]

156156lookupCtxt ns n ctxt = map snd (lookupCtxtName ns n ctxt)

157157

158+updateDef :: Name -> (a -> a) -> Ctxt a -> Ctxt a

159+updateDef n f ctxt

160+ = let ds = lookupCtxtName Nothing n ctxt in

161+ foldr (\ (n, t) c -> addDef n (f t) c) ctxt ds

162+

158163toAlist :: Ctxt a -> [(Name, a)]

159164toAlist ctxt = let allns = map snd (Map.toList ctxt) in

160165 concat (map (Map.toList) allns)

src/Idris/AbsSyntax.hs+13−1

@@ -64,6 +64,7 @@ data IBCWrite = IBCFix FixDecl

6464 | IBCObj FilePath

6565 | IBCLib String

6666 | IBCHeader String

67+ | IBCAccess Name Accessibility

6768 | IBCDef Name -- i.e. main context

6869 deriving Show

6970

@@ -92,6 +93,12 @@ addLib f = do i <- get; put (i { idris_libs = f : idris_libs i })

9293addHdr :: String -> Idris ()

9394addHdr f = do i <- get; put (i { idris_hdrs = f : idris_hdrs i })

9495

96+setAccessibility :: Name -> Accessibility -> Idris ()

97+setAccessibility n a

98+ = do i <- get

99+ let ctxt = setAccess n a (tt_ctxt i)

100+ put (i { tt_ctxt = ctxt })

101+

95102addIBC :: IBCWrite -> Idris ()

96103addIBC ibc = do i <- get; put (i { ibc_write = ibc : ibc_write i })

97104

@@ -298,7 +305,7 @@ inlinable :: FnOpts -> Bool

298305inlinable = elem Inlinable

299306

300307data PDecl' t = PFix FC Fixity [String] -- fixity declaration

301− | PTy SyntaxInfo FC Name t -- type declaration

308+ | PTy SyntaxInfo FC Name t -- type declaration

302309 | PClauses FC FnOpts Name [PClause' t] -- pattern clause

303310 | PData SyntaxInfo FC (PData' t) -- data declaration

304311 | PParams FC [(Name, t)] [PDecl' t] -- params block

@@ -640,7 +647,12 @@ showImp impl tm = se 10 tm where

640647 se p (PProof ts) = "proof { " ++ show ts ++ "}"

641648 se p (PTactics ts) = "tactics { " ++ show ts ++ "}"

642649 se p (PMetavar n) = "?" ++ show n

650+ se p (PReturn f) = "return"

651+ se p PImpossible = "impossible"

643652 se p Placeholder = "_"

653+ se p (PDoBlock _) = "do block show not implemented"

654+ se p (PElabError s) = s

655+-- se p x = "Not implemented"

644656

645657 sArg (PImp _ _ n tm) = siArg (n, tm)

646658 sArg (PExp _ _ tm) = seArg tm

src/Idris/ElabTerm.hs+1−1

@@ -200,7 +200,7 @@ elab ist info pattern fn tm

200200 elab' (PProof ts) = do mapM_ (runTac True ist) ts

201201 elab' (PTactics ts) = do mapM_ (runTac False ist) ts

202202 elab' (PElabError e) = fail e

203− elab' x = fail $ "Not implemented " ++ show x

203+ elab' x = fail $ "Something's gone wrong. Did you miss a semi-colon somewhere?"

204204

205205 elabArgs failed retry [] _

206206 | retry = let (ns, ts) = unzip (reverse failed) in

src/Idris/IBC.hs+29−6

@@ -22,7 +22,7 @@ import System.Posix.Files

2222import Paths_idris

2323

2424ibcVersion :: Word8

25−ibcVersion = 3

25+ibcVersion = 4

2626

2727data IBCFile = IBCFile { ver :: Word8,

2828 sourcefile :: FilePath,

@@ -36,13 +36,14 @@ data IBCFile = IBCFile { ver :: Word8,

3636 ibc_objs :: [FilePath],

3737 ibc_libs :: [String],

3838 ibc_hdrs :: [String],

39+ ibc_access :: [(Name, Accessibility)],

3940 ibc_defs :: [(Name, Def)] }

4041{-!

4142deriving instance Binary IBCFile

4243!-}

4344

4445initIBC :: IBCFile

45−initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] []

46+initIBC = IBCFile ibcVersion "" [] [] [] [] [] [] [] [] [] [] [] []

4647

4748loadIBC :: FilePath -> Idris ()

4849loadIBC fp = do iLOG $ "Loading ibc " ++ fp

@@ -87,8 +88,9 @@ ibc i (IBCObj n) f = return f { ibc_objs = n : ibc_objs f }

8788ibc i (IBCLib n) f = return f { ibc_libs = n : ibc_libs f }

8889ibc i (IBCHeader n) f = return f { ibc_hdrs = n : ibc_hdrs f }

8990ibc i (IBCDef n) f = case lookupDef Nothing n (tt_ctxt i) of

90− [v] -> return f { ibc_defs = (n,v): ibc_defs f }

91+ [v] -> return f { ibc_defs = (n,v) : ibc_defs f }

9192 _ -> fail "IBC write failed"

93+ibc i (IBCAccess n a) f = return f { ibc_access = (n,a) : ibc_access f }

9294

9395process :: IBCFile -> FilePath -> Idris ()

9496process i fn

@@ -107,6 +109,7 @@ process i fn

107109 pLibs (ibc_libs i)

108110 pHdrs (ibc_hdrs i)

109111 pDefs (ibc_defs i)

112+ pAccess (ibc_access i)

110113

111114timestampOlder :: FilePath -> FilePath -> IO ()

112115timestampOlder src ibc = do srcok <- doesFileExist src

@@ -180,7 +183,12 @@ pDefs ds = mapM_ (\ (n, d) ->

180183 do i <- getIState

181184 putIState (i { tt_ctxt = addCtxtDef n d (tt_ctxt i) }))

182185 ds

183−

186+

187+pAccess :: [(Name, Accessibility)] -> Idris ()

188+pAccess ds = mapM_ (\ (n, a) ->

189+ do i <- getIState

190+ putIState (i { tt_ctxt = setAccess n a (tt_ctxt i) }))

191+ ds

184192

185193----- Generated by 'derive'

186194

@@ -505,9 +513,22 @@ instance Binary Def where

505513 return (CaseOp x1 x2 x3 x4 x5)

506514 _ -> error "Corrupted binary data for Def"

507515

516+instance Binary Accessibility where

517+ put x

518+ = case x of

519+ Public -> putWord8 0

520+ Frozen -> putWord8 1

521+ Hidden -> putWord8 2

522+ get

523+ = do i <- getWord8

524+ case i of

525+ 0 -> return Public

526+ 1 -> return Frozen

527+ 2 -> return Hidden

528+ _ -> error "Corrupted binary data for Accessibility"

508529

509530instance Binary IBCFile where

510− put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

531+ put (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

511532 = do put x1

512533 put x2

513534 put x3

@@ -521,6 +542,7 @@ instance Binary IBCFile where

521542 put x11

522543 put x12

523544 put x13

545+ put x14

524546 get

525547 = do x1 <- get

526548 if x1 == ibcVersion then

@@ -536,7 +558,8 @@ instance Binary IBCFile where

536558 x11 <- get

537559 x12 <- get

538560 x13 <- get

539− return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

561+ x14 <- get

562+ return (IBCFile x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

540563 else return (initIBC { ver = x1 })

541564

542565instance Binary Fixity where

src/Idris/Parser.hs+6

@@ -862,6 +862,12 @@ pDirective = try (do lchar '%'; reserved "lib"; lib <- strlit;

862862 <|> try (do lchar '%'; reserved "include"; hdr <- strlit;

863863 return [PDirective (do addHdr hdr

864864 addIBC (IBCHeader hdr))])

865+ <|> try (do lchar '%'; reserved "hide"; n <- iName []

866+ return [PDirective (do setAccessibility n Hidden

867+ addIBC (IBCAccess n Hidden))])

868+ <|> try (do lchar '%'; reserved "freeze"; n <- iName []

869+ return [PDirective (do setAccessibility n Frozen

870+ addIBC (IBCAccess n Frozen))])

865871 <|> do lchar '%'; reserved "logging"; i <- natural;

866872 return [PDirective (setLogLevel (fromInteger i))]

867873

tutorial/typesfuns.tex+20−2

@@ -198,12 +198,14 @@ Ambiguous constructor names can normally be resolved from context.

198198

199199This declares a family of types, and so the form of the declaration is rather

200200different from the simple type declarations above. We explicitly state the type

201−of the type constructor \tTC{Vect} - it takes a type and a \tTC{Nat} as an

201+of the type constructor \tTC{Vect} --- it takes a type and a \tTC{Nat} as an

202202argument, where \tTC{Set} stands for the type of types. We say that \tTC{Vect}

203203is \emph{parameterised} by a type, and \emph{indexed} over \tTC{Nat}. Each

204204constructor targets a different part of the family of types. \tDC{Nil} can only

205205be used to construct vectors with zero length, and \tDC{::} to constructor

206−vectors with non-zero length.

206+vectors with non-zero length. In the type of \tDC{::}, we state explicitly that an element

207+of type \texttt{a} and a tail of type \texttt{Vect a k} (i.e., a vector of length \texttt{k})

208+combine to make a vector of length \texttt{S k}.

207209

208210We can define functions on dependent types such as \tTC{Vect} in the same way

209211as on simple types such as \tTC{List} and \tTC{Nat} above, by pattern matching.

@@ -295,6 +297,22 @@ since it would force \texttt{n} to be \tDC{O}.

295297

296298\subsubsection{Dependent Function Types}

297299

300+The function types we have seen so far have taken the form \texttt{a -> b},

301+where \texttt{a} stands for the input type and \texttt{b} stands for the output

302+type. More generally, function types take the following form:

303+

304+\begin{SaveVerbatim}{ftype}

305+

306+(x : a) -> b

307+

308+\end{SaveVerbatim}

309+\useverb{ftype}

310+

311+\noindent

312+\ldots where the name \texttt{x} may appear in \texttt{b}. This is a \remph{dependent}

313+function type --- the output type depends on the value of \texttt{x}.

314+

315+

298316\subsubsection{Implicit Arguments}

299317

300318\subsection{Useful Data Types}