Language.TypeTheory


   0 | ||| The content of this module is based on the paper:
   1 | ||| A tutorial implementation of a dependently typed lambda calculus
   2 | ||| by Andres Löh, Conor McBride, and Wouter Swierstra
   3 | |||
   4 | ||| NB: The work is originally written in Haskell and uses unsafe features
   5 | |||     This is not how we would write idiomatic Idris code.
   6 | |||     Cf. Language.IntrinsicScoping.TypeTheory for a more idiomatic representation.
   7 | module Language.TypeTheory
   8 | 
   9 | import Control.Monad.Error.Interface
  10 | import Data.List
  11 | 
  12 | %hide Prelude.Abs
  13 | %hide Prelude.MkAbs
  14 | 
  15 | %default covering
  16 | 
  17 | private infixl 3 `App`
  18 | 
  19 | ||| We use this wrapper to mark places where binding occurs.
  20 | ||| This is a major footgun and we hope the type constructor
  21 | ||| forces users to think carefully about what they are doing
  22 | ||| when they encounter Abs, thus potentially avoiding scoping bugs
  23 | ||| given that scope is not an invariant here.
  24 | ||| This is unfortunately not present in the original paper.
  25 | data Abs : Type -> Type where
  26 |    ||| The body of an abstraction lives in an extended context
  27 |    MkAbs : t -> Abs t
  28 | 
  29 | Eq t => Eq (Abs t) where
  30 |   MkAbs b == MkAbs b' = b == b'
  31 | 
  32 | ||| Section 2: Simply Typed Lambda Calculus
  33 | namespace Section2
  34 | 
  35 |   -- 2.4: Implementation
  36 | 
  37 |   ||| Named variables
  38 |   public export
  39 |   total
  40 |   data Name : Type where
  41 |     ||| The most typical of name: external functions
  42 |     Global : String -> Name
  43 |     ||| When passing under a binder we convert a bound variable
  44 |     ||| into a `Local` free variable
  45 |     Local : Nat -> Name
  46 |     ||| During quoting from values back to term we will be using
  47 |     ||| the `Quote` constructor
  48 |     Quote : Nat -> Name
  49 | 
  50 |   %name Name nm
  51 | 
  52 |   public export
  53 |   Eq Name where
  54 |     Global m == Global n = m == n
  55 |     Local m == Local n = m == n
  56 |     Quote m == Quote n = m == n
  57 |     _ == _ = False
  58 | 
  59 |   private infixr 0 ~>
  60 |   total
  61 |   data Ty : Type where
  62 |     ||| A family of base types
  63 |     Base : Name -> Ty
  64 |     ||| A function type from
  65 |     ||| @i the type of the function's input to
  66 |     ||| @o the type of the function's output
  67 |     (~>) : (i, o : Ty) -> Ty
  68 | 
  69 |   %name Ty a, b
  70 | 
  71 |   Eq Ty where
  72 |     Base m == Base n = m == n
  73 |     (i ~> o) == (a ~> b) = i == a && o == b
  74 |     _ == _ = False
  75 | 
  76 |   -- Raw terms are neither scopechecked nor typecked
  77 | 
  78 |   ||| Inferrable terms know what their type is
  79 |   data Infer : Type
  80 | 
  81 |   ||| Checkable terms need to be checked against a type
  82 |   data Check : Type
  83 | 
  84 |   total
  85 |   data Infer : Type where
  86 |     ||| A checkable term annotated with its expected type
  87 |     Ann : Check -> Ty -> Infer
  88 |     ||| A bound variable
  89 |     Bnd : Nat -> Infer
  90 |     ||| A free variable
  91 |     Var : Name -> Infer
  92 |     ||| The application of a function to its argument
  93 |     App : Infer -> Check -> Infer
  94 | 
  95 |   %name Infer e, f
  96 | 
  97 |   total
  98 |   data Check : Type where
  99 |     ||| Inferrable terms are trivially checkable
 100 |     Emb : Infer -> Check
 101 |     ||| A function binding its argument
 102 |     Lam : Abs Check -> Check
 103 | 
 104 |   substCheck : Nat -> Infer -> Check -> Check
 105 |   substAbs   : Nat -> Infer -> Abs Check -> Abs Check
 106 |   substInfer : Nat -> Infer -> Infer -> Infer
 107 | 
 108 |   substCheck lvl u (Emb t) = Emb (substInfer lvl u t)
 109 |   substCheck lvl u (Lam b) = Lam (substAbs lvl u b)
 110 | 
 111 |   substAbs lvl u (MkAbs t) = MkAbs (substCheck (S lvl) u t)
 112 | 
 113 |   substInfer lvl u (Ann s a) = Ann (substCheck lvl u s) a
 114 |   substInfer lvl u (Bnd k) = ifThenElse (lvl == k) u (Bnd k)
 115 |   substInfer lvl u (Var nm) = Var nm
 116 |   substInfer lvl u (App e s) = App (substInfer lvl u e) (substCheck lvl u s)
 117 | 
 118 |   applyAbs : Abs Check -> Infer -> Check
 119 |   applyAbs (MkAbs t) u = substCheck 0 u t
 120 | 
 121 |   %name Check s, t
 122 | 
 123 |   data Value : Type
 124 |   data Stuck : Type
 125 | 
 126 |   ||| Unsafe type of values
 127 |   data Value : Type where
 128 |     ||| Lambda abstractions become functions in the host language
 129 |     VLam : (Value -> Value) -> Value
 130 |     ||| Stuck computations qualify as values
 131 |     VEmb : Stuck -> Value
 132 | 
 133 |   ||| Type of stuck computations
 134 |   data Stuck : Type where
 135 |     ||| A variable is a stuck computation
 136 |     NVar : Name -> Stuck
 137 |     ||| An application whose function is stuck is also stuck
 138 |     NApp : Stuck -> Value -> Stuck
 139 | 
 140 |   ||| We can easily turn a name into a value
 141 |   ||| by building a stuck computation first
 142 |   vfree : Name -> Value
 143 |   vfree x = VEmb (NVar x)
 144 | 
 145 |   ||| We can easily apply a value standing for a function
 146 |   ||| to a value standing for its argument by either deploying
 147 |   ||| the function or growing the spine of the stuck computation.
 148 |   vapp : Value -> Value -> Value
 149 |   vapp (VLam f) t = f t
 150 |   vapp (VEmb n) t = VEmb (NApp n t)
 151 | 
 152 |   ||| An environment is a list of values for all the bound variables in scope
 153 |   Env : Type
 154 |   Env = List Value
 155 | 
 156 |   ||| Big step evaluation of an inferrable term in a given environment
 157 |   partial
 158 |   evalInfer : Infer -> Env -> Value
 159 | 
 160 |   ||| Big step evaluation of a checkable term in a given environment
 161 |   partial
 162 |   evalCheck : Check -> Env -> Value
 163 | 
 164 |   ||| Big step evaluation of an abstraction's body
 165 |   partial
 166 |   evalAbs : Abs Check -> Env -> Value -> Value
 167 |   evalAbs (MkAbs t) env v = evalCheck t (v :: env)
 168 | 
 169 |   evalInfer (Ann t _) env = evalCheck t env
 170 |   evalInfer (Bnd x) env = case inBounds x env of
 171 |     Yes prf => index x env
 172 |     No nprf => idris_crash "INTERNAL ERROR: evalInfer -> impossible case"
 173 |   evalInfer (Var x) env = vfree x
 174 |   evalInfer (App f t) env = vapp (evalInfer f env) (evalCheck t env)
 175 | 
 176 |   evalCheck (Emb i) env = evalInfer i env
 177 |   evalCheck (Lam b) env = VLam (evalAbs b env)
 178 | 
 179 | 
 180 |   data Kind =
 181 |     ||| We have a unique kind star for known base types
 182 |     Star
 183 | 
 184 |   ||| Names in scope either have an associated
 185 |   ||| Kind (they're base types) or
 186 |   ||| Ty (they're term variables)
 187 |   data Info : Type where
 188 |     HasKind : Kind -> Info
 189 |     HasType : Ty -> Info
 190 | 
 191 |   ||| A context is a list of names and their associated info
 192 |   Context : Type
 193 |   Context = List (Name, Info)
 194 | 
 195 |   parameters {0 m : Type -> Type} {auto _ : MonadError String m}
 196 | 
 197 |     ||| Checking a type's kinding
 198 |     kind : Context -> Kind -> Ty -> m ()
 199 |     kind ctx Star (Base x) = do
 200 |       let Just (HasKind Star) = lookup x ctx
 201 |          | Just _ => throwError "invalid identifier"
 202 |          | _ => throwError "unknown identifier"
 203 |       pure ()
 204 |     kind ctx Star (i ~> o) = do
 205 |       kind ctx Star i
 206 |       kind ctx Star o
 207 | 
 208 |     ||| Inference
 209 |     inferI : Nat -> Context -> Infer -> m Ty
 210 |     ||| Checking
 211 |     checkI : Nat -> Context -> Ty -> Check -> m ()
 212 | 
 213 |     inferI lvl ctx (Ann t ty) = do
 214 |       kind ctx Star ty
 215 |       ty <$ checkI lvl ctx ty t
 216 |     inferI lvl ctx (Bnd x) =
 217 |       -- unhandled in the original Haskell
 218 |       throwError "Oops"
 219 |     inferI lvl ctx (Var v) = do
 220 |       let Just (HasType ty) = lookup v ctx
 221 |         | Just _ => throwError "invalid identifier"
 222 |         | _ => throwError "unknown identifier"
 223 |       pure ty
 224 |     inferI lvl ctx (App f t) = do
 225 |       (i ~> o) <- inferI lvl ctx f
 226 |         | _ => throwError "illegal application"
 227 |       o <$ checkI lvl ctx i t
 228 | 
 229 | 
 230 |     checkI lvl ctx ty (Emb t) = do
 231 |       ty' <- inferI lvl ctx t
 232 |       unless (ty == ty') $ throwError "type mismatch"
 233 | 
 234 |     checkI lvl ctx ty (Lam b) = do
 235 |       let (i ~> o) = ty
 236 |         | _ => throwError "expected a function type"
 237 |       let x = Local lvl
 238 |       let k = HasType i
 239 |       let b = applyAbs b (Var x)
 240 |       checkI (S lvl) ((x, k) :: ctx) o b
 241 | 
 242 |     infer : Context -> Infer -> m Ty
 243 |     infer = inferI 0
 244 | 
 245 |     check : Context -> Ty -> Check -> m ()
 246 |     check = checkI 0
 247 | 
 248 |   exampleC : check [(Global "o", HasKind Star)]
 249 |                    (let ty = Base (Global "o") in (ty ~> ty) ~> ty ~> ty)
 250 |                    (Lam (MkAbs (Lam (MkAbs (Emb (Bnd 0))))))
 251 |            = Right {a = String} ()
 252 |   exampleC = Refl
 253 | 
 254 |   boundFree : Nat -> Name -> Infer
 255 |   boundFree lvl (Quote i) = Bnd (minus lvl (S i))
 256 |   boundFree lvl x = Var x
 257 | 
 258 |   quoteStuckI : Nat -> Stuck -> Infer
 259 |   quoteValueI : Nat -> Value -> Check
 260 |   quoteAbsI   : Nat -> (Value -> Value) -> Abs Check
 261 | 
 262 |   quoteStuckI lvl (NVar nm) = boundFree lvl nm
 263 |   quoteStuckI lvl (NApp e t) = App (quoteStuckI lvl e) (quoteValueI lvl t)
 264 | 
 265 |   quoteValueI lvl (VLam f) = Lam (quoteAbsI lvl f)
 266 |   quoteValueI lvl (VEmb e) = Emb (quoteStuckI lvl e)
 267 | 
 268 |   quoteAbsI lvl f = MkAbs (quoteValueI (S lvl) (f (vfree (Quote lvl))))
 269 | 
 270 |   quoteValue : Value -> Check
 271 |   quoteValue = quoteValueI 0
 272 | 
 273 |   partial
 274 |   normCheck : Check -> Env -> Check
 275 |   normCheck t env = quoteValue (evalCheck t env)
 276 | 
 277 |   partial
 278 |   normInfer : Infer -> Env -> Check
 279 |   normInfer t env = quoteValue (evalInfer t env)
 280 | 
 281 |   exampleQ : quoteValue (VLam $ \x => VLam $ \y => x)
 282 |            = Lam (MkAbs (Lam (MkAbs (Emb (Bnd 1)))))
 283 |   exampleQ = Refl
 284 | 
 285 | 
 286 |   namespace Infer
 287 |     public export
 288 |     fromInteger : Integer -> Infer
 289 |     fromInteger n = Bnd (cast n)
 290 | 
 291 |   namespace Check
 292 |     public export
 293 |     fromString : String -> Check
 294 |     fromString x = Emb (Var (Global x))
 295 | 
 296 |     public export
 297 |     fromInteger : Integer -> Check
 298 |     fromInteger n = Emb (Bnd (cast n))
 299 | 
 300 |   ID, CONST : Check
 301 |   ID = Lam (MkAbs 0)
 302 |   CONST = Lam (MkAbs (Lam (MkAbs 1)))
 303 | 
 304 |   namespace Ty
 305 |     public export
 306 |     fromString : String -> Ty
 307 |     fromString x = Base (Global x)
 308 | 
 309 |   Term1 : Infer
 310 |   Term1 = Ann ID ("a" ~> "a") `App` "y"
 311 | 
 312 |   Ctx1 : Context
 313 |   Ctx1 = [(Global "y", HasType "a"), (Global "a", HasKind Star)]
 314 | 
 315 |   Term2 : Infer
 316 |   Term2 = Ann CONST (("b" ~> "b") ~> "a" ~> "b" ~> "b")
 317 |           `App` ID `App` "y"
 318 | 
 319 |   Ctx2 : Context
 320 |   Ctx2 = (Global "b", HasKind Star) :: Ctx1
 321 | 
 322 |   test0 : normInfer Term1 [] === "y"
 323 |   test0 = Refl
 324 | 
 325 |   test1 : normInfer Term2 [] === ID
 326 |   test1 = Refl
 327 | 
 328 |   test2 : infer Ctx1 Term1 === Right {a = String} "a"
 329 |   test2 = Refl
 330 | 
 331 |   test3 : infer Ctx2 Term2 === Right {a = String} ("b" ~> "b")
 332 |   test3 = Refl
 333 | 
 334 | %hide Infer
 335 | %hide Check
 336 | %hide Value
 337 | %hide Stuck
 338 | 
 339 | namespace Section3
 340 | 
 341 |   -- 3.4: Implementation
 342 | 
 343 |   data Infer : Type
 344 |   data Check : Type
 345 | 
 346 |   total
 347 |   data Infer : Type where
 348 |     ||| A checkable term annotated with its expected type
 349 |     Ann : (t, ty : Check) -> Infer
 350 |     ||| The star kind is inferrable
 351 |     Star : Infer
 352 |     ||| Pi is inferrable
 353 |     Pi : (a : Check) -> (b : Abs Check) -> Infer
 354 |     ||| A bound variable
 355 |     Bnd : (k : Nat) -> Infer
 356 |     ||| A free variable
 357 |     Var : (nm : Name) -> Infer
 358 |     ||| The application of a function to its argument
 359 |     App : Infer -> Check -> Infer
 360 | 
 361 | 
 362 |   %name Infer e, f
 363 | 
 364 |   total
 365 |   data Check : Type where
 366 |     ||| Inferrable terms are trivially checkable
 367 |     Emb : Infer -> Check
 368 |     ||| A function binding its argument
 369 |     Lam : Abs Check -> Check
 370 | 
 371 |   Eq Infer
 372 |   Eq Check
 373 | 
 374 |   Eq Infer where
 375 |     Ann t ty == Ann t' ty' = t == t' && ty == ty'
 376 |     Star == Star = True
 377 |     Pi a b == Pi s t = a == s && assert_total (b == t)
 378 |     Bnd k == Bnd l = k == l
 379 |     Var m == Var n = m == n
 380 |     App e s == App f t = e == f && s == t
 381 |     _ == _ = False
 382 | 
 383 |   Eq Check where
 384 |     Emb e == Emb f = assert_total (e == f)
 385 |     Lam b == Lam t = assert_total (b == t)
 386 |     _ == _ = False
 387 | 
 388 |   substCheck : Nat -> Infer -> Check -> Check
 389 |   substAbs   : Nat -> Infer -> Abs Check -> Abs Check
 390 |   substInfer : Nat -> Infer -> Infer -> Infer
 391 | 
 392 |   substAbs lvl u (MkAbs b) = MkAbs (substCheck (S lvl) u b)
 393 | 
 394 | 
 395 |   substCheck lvl u (Emb t) = Emb (substInfer lvl u t)
 396 |   substCheck lvl u (Lam b) = Lam (substAbs lvl u b)
 397 | 
 398 |   substInfer lvl u (Ann s a) = Ann (substCheck lvl u s) (substCheck lvl u a)
 399 |   substInfer lvl u Star = Star
 400 |   substInfer lvl u (Pi a b) = Pi (substCheck lvl u a) (substAbs lvl u b)
 401 |   substInfer lvl u (Bnd k) = ifThenElse (lvl == k) u (Bnd k)
 402 |   substInfer lvl u (Var nm) = Var nm
 403 |   substInfer lvl u (App e s) = App (substInfer lvl u e) (substCheck lvl u s)
 404 | 
 405 |   applyAbs : Abs Check -> Infer -> Check
 406 |   applyAbs (MkAbs t) u = substCheck 0 u t
 407 | 
 408 |   %name Check s, t
 409 | 
 410 |   data Value : Type
 411 |   data Stuck : Type
 412 | 
 413 |   data Value : Type where
 414 |     ||| Lambda abstractions become functions in the host language
 415 |     VLam  : (b : Value -> Value) -> Value
 416 |     ||| The Star kind is a value already
 417 |     VStar : Value
 418 |     ||| Pi constructors combine a value for their domain and
 419 |     ||| a function in the host language for their codomain
 420 |     VPi   : (a : Value) -> (b : Value -> Value) -> Value
 421 |     ||| Stuck computations qualify as values
 422 |     VEmb  : (e : Stuck) -> Value
 423 | 
 424 |   data Stuck : Type where
 425 |     ||| A variable is a stuck computation
 426 |     NVar : Name -> Stuck
 427 |     ||| An application whose function is stuck is also stuck
 428 |     NApp : Stuck -> Value -> Stuck
 429 | 
 430 |   ||| Types are just values in TT
 431 |   Ty : Type
 432 |   Ty = Value
 433 | 
 434 |   ||| A context maps names to types, that is to say values
 435 |   Context : Type
 436 |   Context = List (Name, Ty)
 437 | 
 438 |   ||| We can easily turn a name into a value
 439 |   ||| by building a stuck computation first
 440 |   vfree : Name -> Value
 441 |   vfree x = VEmb (NVar x)
 442 | 
 443 |   ||| We can easily apply a value standing for a function
 444 |   ||| to a value standing for its argument by either deploying
 445 |   ||| the function or growing the spine of the stuck computation.
 446 |   partial
 447 |   vapp : Value -> Value -> Value
 448 |   vapp (VLam f) t = f t
 449 |   vapp (VEmb n) t = VEmb (NApp n t)
 450 |   vapp _ _ = idris_crash "INTERNAL ERROR: vapp -> impossible case"
 451 | 
 452 |   ||| An environment is a list of values for all the bound variables in scope
 453 |   Env : Type
 454 |   Env = List Value
 455 | 
 456 |   ||| Big step evaluation of an inferrable term in a given environment
 457 |   partial
 458 |   evalInfer : Infer -> Env -> Value
 459 | 
 460 |   ||| Big step evaluation of a checkable term in a given environment
 461 |   partial
 462 |   evalCheck : Check -> Env -> Value
 463 | 
 464 |   partial
 465 |   evalAbs : Abs Check -> Env -> Value -> Value
 466 |   evalAbs (MkAbs t) env v = evalCheck t (v :: env)
 467 | 
 468 | 
 469 |   evalInfer (Ann t _) env = evalCheck t env
 470 |   evalInfer Star env = VStar
 471 |   evalInfer (Pi a b) env = VPi (evalCheck a env) (evalAbs b env)
 472 |   evalInfer (Bnd x) env = case inBounds x env of
 473 |     Yes prf => index x env
 474 |     No nprf => idris_crash "INTERNAL ERROR: evalInfer -> impossible case"
 475 |   evalInfer (Var x) env = vfree x
 476 |   evalInfer (App f t) env = vapp (evalInfer f env) (evalCheck t env)
 477 | 
 478 |   evalCheck (Emb i) env = evalInfer i env
 479 |   evalCheck (Lam b) env = VLam (evalAbs b env)
 480 | 
 481 | 
 482 |   boundFree : Nat -> Name -> Infer
 483 |   boundFree lvl (Quote i) = Bnd (minus lvl (S i))
 484 |   boundFree lvl x = Var x
 485 | 
 486 |   quoteStuckI : Nat -> Stuck -> Infer
 487 |   quoteValueI : Nat -> Value -> Check
 488 |   quoteAbsI   : Nat -> (Value -> Value) -> Abs Check
 489 | 
 490 |   quoteStuckI lvl (NVar nm) = boundFree lvl nm
 491 |   quoteStuckI lvl (NApp e t) = App (quoteStuckI lvl e) (quoteValueI lvl t)
 492 | 
 493 |   quoteValueI lvl VStar = Emb Star
 494 |   quoteValueI lvl (VPi a b)
 495 |     = let a = quoteValueI lvl a in
 496 |       let b = quoteAbsI lvl b in
 497 |       Emb (Pi a b)
 498 |   quoteValueI lvl (VLam f) = Lam (quoteAbsI lvl f)
 499 |   quoteValueI lvl (VEmb e) = Emb (quoteStuckI lvl e)
 500 | 
 501 |   quoteAbsI lvl f =
 502 |     let x = vfree (Quote lvl) in
 503 |     MkAbs (quoteValueI (S lvl) (f x))
 504 | 
 505 | 
 506 |   quoteValue : Value -> Check
 507 |   quoteValue = quoteValueI 0
 508 | 
 509 |   partial
 510 |   normCheck : Check -> Env -> Check
 511 |   normCheck t env = quoteValue (evalCheck t env)
 512 | 
 513 |   partial
 514 |   normInfer : Infer -> Env -> Check
 515 |   normInfer t env = quoteValue (evalInfer t env)
 516 | 
 517 |   parameters {0 m : Type -> Type} {auto _ : MonadError String m}
 518 | 
 519 |     inferI    : Nat -> Context -> Infer -> m Ty
 520 |     checkI    : Nat -> Context -> Ty -> Check -> m ()
 521 |     checkAbsI : Nat -> Context -> Ty -> (Ty -> Ty) -> Abs Check -> m ()
 522 | 
 523 |     inferI lvl ctx (Ann t ty) = do
 524 |       checkI lvl ctx VStar ty
 525 |       let ty = assert_total (evalCheck ty [])
 526 |       ty <$ checkI lvl ctx ty t
 527 |     inferI lvl ctx Star = pure VStar
 528 |     inferI lvl ctx (Pi a b) = do
 529 |       checkI lvl ctx VStar a
 530 |       let a = assert_total (evalCheck a [])
 531 |       let x = Local lvl
 532 |       VStar <$ checkAbsI lvl ctx a (\ _ => VStar) b
 533 |     inferI lvl ctx (Bnd k) =
 534 |       -- unhandled in the original Haskell
 535 |       throwError "Oops"
 536 |     inferI lvl ctx (Var v) = do
 537 |       let Just ty = lookup v ctx
 538 |         | _ => throwError "unknown identifier"
 539 |       pure ty
 540 |     inferI lvl ctx (App f t) = do
 541 |       (VPi a b) <- inferI lvl ctx f
 542 |         | _ => throwError "illegal application"
 543 |       checkI lvl ctx a t
 544 |       let t = assert_total (evalCheck t [])
 545 |       pure (b t)
 546 | 
 547 | 
 548 |     checkI lvl ctx ty (Emb t) = do
 549 |       ty' <- inferI lvl ctx t
 550 |       unless (quoteValue ty == quoteValue ty') $ throwError "type mismatch"
 551 |     checkI lvl ctx ty (Lam t) = do
 552 |       let VPi a b = ty
 553 |         | _ => throwError "expected a function type"
 554 |       checkAbsI lvl ctx a b t
 555 | 
 556 |   checkAbsI lvl ctx a b t = do
 557 |       let x = Local lvl
 558 |       let b = b (vfree x)
 559 |       let t = applyAbs t (Var x)
 560 |       checkI (S lvl) ((x, a) :: ctx) b t
 561 | 
 562 | %hide Infer
 563 | %hide Check
 564 | 
 565 | ||| Section 4: Beyond LambdaPi
 566 | namespace Section4
 567 | 
 568 |   -- Section 4.1 Implementing natural numbers
 569 | 
 570 |   data Infer : Type
 571 |   data Check : Type
 572 | 
 573 |   total
 574 |   data Infer : Type where
 575 |     ||| A checkable term annotated with its expected type
 576 |     Ann : (t, ty : Check) -> Infer
 577 |     ||| The star kind is inferrable
 578 |     Star : Infer
 579 |     ||| The nat type is inferrable
 580 |     Nat : Infer
 581 |     ||| The nat induction principle is inferrable
 582 |     -- Here there's a bit of leeway in the design: we could just as well demand:
 583 |     --   pred : Abs Check
 584 |     --   pz : Check
 585 |     --   ps : Abs (Abs Check)
 586 |     --   n : Check
 587 |     Rec : (pred, pz, ps : Check) -> (n : Check) -> Infer
 588 |     ||| The zero constructor is inferrable
 589 |     Zro : Infer
 590 |     ||| The successor constructor is inferrable
 591 |     Suc : Check -> Infer
 592 |     ||| Pi is inferrable
 593 |     Pi : (a : Check) -> (b : Abs Check) -> Infer
 594 |     ||| A bound variable
 595 |     Bnd : (k : Nat) -> Infer
 596 |     ||| A free variable
 597 |     Var : (nm : Name) -> Infer
 598 |     ||| The application of a function to its argument
 599 |     App : Infer -> Check -> Infer
 600 | 
 601 |   %name Infer e, f
 602 | 
 603 |   total
 604 |   data Check : Type where
 605 |     ||| Inferrable terms are trivially checkable
 606 |     Emb : Infer -> Check
 607 |     ||| A function binding its argument
 608 |     Lam : Abs Check -> Check
 609 | 
 610 |   Eq Infer
 611 |   Eq Check
 612 | 
 613 |   Eq Infer where
 614 |     Ann t ty == Ann t' ty' = t == t' && ty == ty'
 615 |     Star == Star = True
 616 |     Pi a b == Pi s t = a == s && b == t
 617 |     Bnd k == Bnd l = k == l
 618 |     Var m == Var n = m == n
 619 |     App e s == App f t = e == f && s == t
 620 |     _ == _ = False
 621 | 
 622 |   Eq Check where
 623 |     Emb e == Emb f = assert_total (e == f)
 624 |     Lam b == Lam t = assert_total (b == t)
 625 |     _ == _ = False
 626 | 
 627 |   substCheck : Nat -> Infer -> Check -> Check
 628 |   substAbs   : Nat -> Infer -> Abs Check -> Abs Check
 629 |   substInfer : Nat -> Infer -> Infer -> Infer
 630 | 
 631 |   substCheck lvl u (Emb t) = Emb (substInfer lvl u t)
 632 |   substCheck lvl u (Lam b) = Lam (substAbs lvl u b)
 633 | 
 634 |   substInfer lvl u (Ann s a) = Ann (substCheck lvl u s) (substCheck lvl u a)
 635 |   substInfer lvl u Star = Star
 636 |   substInfer lvl u Nat = Nat
 637 |   substInfer lvl u Zro = Zro
 638 |   substInfer lvl u (Suc n) = Suc (substCheck lvl u n)
 639 |   substInfer lvl u (Rec p pz ps n)
 640 |     = Rec (substCheck lvl u p) (substCheck lvl u pz) (substCheck lvl u ps) (substCheck lvl u n)
 641 |   substInfer lvl u (Pi a b) = Pi (substCheck lvl u a) (substAbs lvl u b)
 642 |   substInfer lvl u (Bnd k) = ifThenElse (lvl == k) u (Bnd k)
 643 |   substInfer lvl u (Var nm) = Var nm
 644 |   substInfer lvl u (App e s) = App (substInfer lvl u e) (substCheck lvl u s)
 645 | 
 646 |   substAbs lvl u (MkAbs t) = MkAbs (substCheck (S lvl) u t)
 647 | 
 648 |   applyAbs : Abs Check -> Infer -> Check
 649 |   applyAbs (MkAbs t) u = substCheck 0 u t
 650 | 
 651 |   %name Check s, t
 652 | 
 653 |   data Value : Type
 654 |   data Stuck : Type
 655 | 
 656 |   data Value : Type where
 657 |     ||| Lambda abstractions become functions in the host language
 658 |     VLam  : (b : Value -> Value) -> Value
 659 |     ||| The Star kind is a value already
 660 |     VStar : Value
 661 |     ||| The nat type is a value already
 662 |     VNat : Value
 663 |     ||| The zero constructor is avalue
 664 |     VZro : Value
 665 |     ||| The successor constructor is a value constructor
 666 |     VSuc : Value -> Value
 667 |     ||| Pi constructors combine a value for their domain and
 668 |     ||| a function in the host language for their codomain
 669 |     VPi   : (a : Value) -> (b : Value -> Value) -> Value
 670 |     ||| Stuck computations qualify as values
 671 |     VEmb  : (e : Stuck) -> Value
 672 | 
 673 |   data Stuck : Type where
 674 |     ||| A variable is a stuck computation
 675 |     NVar : Name -> Stuck
 676 |     ||| An application whose function is stuck is also stuck
 677 |     NApp : Stuck -> Value -> Stuck
 678 |     ||| An induction principle applied to a stuck natural numnber is stuck
 679 |     NRec : (pred, pz, ps : Value) -> Stuck -> Stuck
 680 | 
 681 |   ||| Types are just values in TT
 682 |   Ty : Type
 683 |   Ty = Value
 684 | 
 685 |   ||| A context maps names to types, that is to say values
 686 |   Context : Type
 687 |   Context = List (Name, Ty)
 688 | 
 689 |   ||| We can easily turn a name into a value
 690 |   ||| by building a stuck computation first
 691 |   vfree : Name -> Value
 692 |   vfree x = VEmb (NVar x)
 693 | 
 694 |   private infixl 5 `vapp`
 695 | 
 696 |   ||| We can easily apply a value standing for a function
 697 |   ||| to a value standing for its argument by either deploying
 698 |   ||| the function or growing the spine of the stuck computation.
 699 |   partial
 700 |   vapp : Value -> Value -> Value
 701 |   vapp (VLam f) t = f t
 702 |   vapp (VEmb n) t = VEmb (NApp n t)
 703 |   vapp _ _ = idris_crash "INTERNAL ERROR: vapp -> impossible case"
 704 | 
 705 |   ||| An environment is a list of values for all the bound variables in scope
 706 |   Env : Type
 707 |   Env = List Value
 708 | 
 709 |   ||| Big step evaluation of an inferrable term in a given environment
 710 |   partial
 711 |   evalInfer : Infer -> Env -> Value
 712 | 
 713 |   ||| Big step evaluation of a checkable term in a given environment
 714 |   partial
 715 |   evalCheck : Check -> Env -> Value
 716 | 
 717 |   ||| Big step evaluation of an abstraction in a given environment
 718 |   partial
 719 |   evalAbs : Abs Check -> Env -> Value -> Value
 720 |   evalAbs (MkAbs t) env v = evalCheck t (v :: env)
 721 | 
 722 |   evalInfer (Ann t _) env = evalCheck t env
 723 |   evalInfer Star env = VStar
 724 |   evalInfer Nat env = VNat
 725 |   evalInfer Zro env = VZro
 726 |   evalInfer (Suc n) env = VSuc (evalCheck n env)
 727 |   evalInfer (Rec p pz ps n) env = go (evalCheck pz env) (evalCheck ps env) (evalCheck n env) where
 728 | 
 729 |     go : (pz, ps, n : Value) -> Value
 730 |     go pz ps VZro = pz
 731 |     go pz ps (VSuc n) = ps `vapp` n `vapp` (go pz ps n)
 732 |     go pz ps (VEmb n) = VEmb (NRec (evalCheck p env) pz ps n)
 733 |     go _ _ _ = idris_crash "INTERNAL ERROR: evalInfer -> impossible case"
 734 | 
 735 |   evalInfer (Pi a b) env = VPi (evalCheck a env) (evalAbs b env)
 736 |   evalInfer (Bnd x) env = case inBounds x env of
 737 |     Yes prf => index x env
 738 |     No nprf => idris_crash "INTERNAL ERROR: evalInfer -> impossible case"
 739 |   evalInfer (Var x) env = vfree x
 740 |   evalInfer (App f t) env = vapp (evalInfer f env) (evalCheck t env)
 741 | 
 742 |   evalCheck (Emb i) env = evalInfer i env
 743 |   evalCheck (Lam b) env = VLam (evalAbs b env)
 744 | 
 745 | 
 746 |   boundFree : Nat -> Name -> Infer
 747 |   boundFree lvl (Quote i) = Bnd (minus lvl (S i))
 748 |   boundFree lvl x = Var x
 749 | 
 750 |   quoteStuckI : Nat -> Stuck -> Infer
 751 |   quoteAbsI   : Nat -> (Value -> Value) -> Abs Check
 752 |   quoteValueI : Nat -> Value -> Check
 753 | 
 754 |   quoteStuckI lvl (NVar nm) = boundFree lvl nm
 755 |   quoteStuckI lvl (NApp e t) = App (quoteStuckI lvl e) (quoteValueI lvl t)
 756 |   quoteStuckI lvl (NRec p pz ps n)
 757 |     = Rec (quoteValueI lvl p) (quoteValueI lvl pz) (quoteValueI lvl ps) (Emb (quoteStuckI lvl n))
 758 | 
 759 |   quoteValueI lvl VStar = Emb Star
 760 |   quoteValueI lvl VNat = Emb Nat
 761 |   quoteValueI lvl VZro = Emb Zro
 762 |   quoteValueI lvl (VSuc n) = Emb (Suc (quoteValueI lvl n))
 763 |   quoteValueI lvl (VPi a b)
 764 |     = let a = quoteValueI lvl a in
 765 |       let b = quoteAbsI lvl b in
 766 |       Emb (Pi a b)
 767 |   quoteValueI lvl (VLam f) = Lam (quoteAbsI lvl f)
 768 |   quoteValueI lvl (VEmb e) = Emb (quoteStuckI lvl e)
 769 | 
 770 |   quoteAbsI lvl f = let x = vfree (Quote lvl) in MkAbs (quoteValueI (S lvl) (f x))
 771 | 
 772 |   quoteValue : Value -> Check
 773 |   quoteValue = quoteValueI 0
 774 | 
 775 |   partial
 776 |   normCheck : Check -> Env -> Check
 777 |   normCheck t env = quoteValue (evalCheck t env)
 778 | 
 779 |   partial
 780 |   normInfer : Infer -> Env -> Check
 781 |   normInfer t env = quoteValue (evalInfer t env)
 782 | 
 783 |   parameters {0 m : Type -> Type} {auto _ : MonadError String m}
 784 | 
 785 |     inferI : Nat -> Context -> Infer -> m Ty
 786 |     checkAbsI : Nat -> Context -> Ty -> (Ty -> Ty) -> Abs Check -> m ()
 787 |     checkI : Nat -> Context -> Ty -> Check -> m ()
 788 | 
 789 |     inferI lvl ctx (Ann t ty) = do
 790 |       checkI lvl ctx VStar ty
 791 |       let ty = assert_total (evalCheck ty [])
 792 |       ty <$ checkI lvl ctx ty t
 793 |     inferI lvl ctx Star = pure VStar
 794 |     inferI lvl ctx Nat = pure VStar
 795 |     inferI lvl ctx Zro = pure VNat
 796 |     inferI lvl ctx (Suc n) = VNat <$ checkI lvl ctx VNat n
 797 |     inferI lvl ctx (Rec p pz ps n) = do
 798 |       -- check & evaluate the predicate
 799 |       checkI lvl ctx (VPi VNat (\ _ => VStar)) p
 800 |       let p = assert_total (evalCheck p [])
 801 |       -- check pz has type (p 0)
 802 |       checkI lvl ctx (assert_total (p `vapp` VZro)) pz
 803 |       -- check ps has type (forall n. p n -> p (1+ n))
 804 |       let psTy = VPi VNat (\ n => VPi (p `vapp` n) (\ _ => p `vapp` VSuc n))
 805 |       checkI lvl ctx psTy ps
 806 |       -- check & evaluate the nat
 807 |       checkI lvl ctx VNat n
 808 |       let n = assert_total (evalCheck n [])
 809 |       -- return (p n)
 810 |       pure (assert_total (p `vapp` n))
 811 |     inferI lvl ctx (Pi a b) = do
 812 |       checkI lvl ctx VStar a
 813 |       let a = assert_total (evalCheck a [])
 814 |       VStar <$ checkAbsI lvl ctx a (\ _ => VStar) b
 815 |     inferI lvl ctx (Bnd k) =
 816 |       -- unhandled in the original Haskell
 817 |       throwError "Oops"
 818 |     inferI lvl ctx (Var v) = do
 819 |       let Just ty = lookup v ctx
 820 |         | _ => throwError "unknown identifier"
 821 |       pure ty
 822 |     inferI lvl ctx (App f t) = do
 823 |       (VPi a b) <- inferI lvl ctx f
 824 |         | _ => throwError "illegal application"
 825 |       checkI lvl ctx a t
 826 |       let t = assert_total (evalCheck t [])
 827 |       pure (b t)
 828 | 
 829 | 
 830 |     checkI lvl ctx ty (Emb t) = do
 831 |       ty' <- inferI lvl ctx t
 832 |       unless (quoteValue ty == quoteValue ty') $ throwError "type mismatch"
 833 |     checkI lvl ctx ty (Lam t) = do
 834 |       let VPi a b = ty
 835 |         | _ => throwError "expected a function type"
 836 |       checkAbsI lvl ctx a b t
 837 | 
 838 | 
 839 |   checkAbsI lvl ctx a b t = do
 840 |       let x = Local lvl
 841 |       let b = b (vfree x)
 842 |       let t = applyAbs t (Var x)
 843 |       checkI (S lvl) ((x, a) :: ctx) b t
 844 |