Documentation

In simple typed lambda calculus one have to define separate functions for different types, even they have same shape.

>>> demo_ basicCtx stlcUnitIdentity
λ x → x : Unit → Unit ↪ λ x → x : Unit → Unit

demo_ prints the term, result of evaluation and checked type

term ↪ value : type

Next we can write identity function for booleans:

>>> demo_ basicCtx stlcBoolIdentity
λ x → x : Bool → Bool ↪ λ x → x : Bool → Bool

If we would write the type-inferencer for STLC (TODO), it would need to default types for such intristically polymorphic values.

As this is the first example, let's see evaluator and type-checker in action:

>>> demo_ basicCtx ("True" :: Term STLC)
True ↪ True : Bool

Next we apply True to the identity function:

>>> demo_ basicCtx $ stlcBoolIdentity @@ "True"
(λ x → x : Bool → Bool) True ↪ True : Bool

If we apply the value of wrong type, we get an error:

>>> demo_ basicCtx $ stlcBoolIdentity @@ "TT"
error:
• Couldn't match expected type Bool with actual type Unit
• In the expression: TT
• when checking expression
  (λ x → x : Bool → Bool) TT

Because the library is based on PTS, we could try to apply a type too, but that's also a type-error:

>>> demo_ basicCtx $ stlcBoolIdentity @@ "Bool"
error:
• Couldn't match expected type Bool with actual type ⋆
• In the expression: Bool
• when checking expression
  (λ x → x : Bool → Bool) Bool

Because simply typed lambda calculus is restrictive, we have polymorphic calculi.

In language-pts we can define the term once and for all specications.

However let's experiment with SystemF first.

>>> demo_ emptyCtx systemfIdentity
λ a x → x : ∀ a → a → a ↪ λ a x → x : ∀ a → a → a

Note: emptyCtx. We can apply values. When we apply a Bool we get boolean identity function, and further we can apply a Value

>>> demo_ basicCtx $ systemfIdentity @@ "Bool"
(λ a x → x : ∀ a → a → a) Bool ↪ λ x → x : Bool → Bool

>>> demo_ basicCtx $ systemfIdentity @@ "Bool" @@ "False"
(λ a x → x : ∀ a → a → a) Bool False ↪ False : Bool

As with STLC, we get type-error if we apply value of wrong type:

>>> demo_ basicCtx $ systemfIdentity @@ "Unit" @@ "False"
error:
• Couldn't match expected type Unit with actual type Bool
• In the expression: False
• when checking expression
  (λ a x → x : ∀ a → a → a) Unit False

And "sort" error, if we try to apply value directly!

>>> demo_ basicCtx $ systemfIdentity @@ "False"
error:
• Couldn't match expected type ⋆ with actual type Bool
• In the expression: False
• when checking expression
  (λ a x → x : ∀ a → a → a) False

Note: we can write polymorphic looking identity function in PTS for STLC, but it won't typecheck:

>>> demo_ emptyCtx stlcIdentity
error:
• No PTS Rule (□,⋆,-)
• when checking expression
  λ a x → x : ∀ a → a → a

In Haskell we can apply identity function to itself

>>> :t id id
id id :: a -> a

GHCs "type-checker" (actually inferrer) infers the following value. Note that all applied types are simple, monomorphic types (no forall_):

>>> demo_ emptyCtx $ lam_ "b" (systemfIdentity @@ ("b" ~> "b") @@ (systemfIdentity @@ "b")) -:- forall_ "b" ("b" ~> "b")
λ b → (λ a x → x : ∀ a → a → a)
          (b → b) ((λ a x → x : ∀ a → a → a) b)
    : ∀ b → b → b
    ↪ λ b x → x : ∀ b → b → b

Alternatively, different value can be inferred (AFAIK that's what Agda would do). Here, as we don't abstract (lam_), we don't need annotations, due bi-directional type-checking in language-pts!

>>> demo_ emptyCtx $ systemfIdentity @@ forall_ "b" ("b" ~> "b") @@@ systemfIdentity
(λ a x → x : ∀ a → a → a)
    (∀ b → b → b) (λ a x → x : ∀ a → a → a)
    ↪ λ a x → x : ∀ b → b → b

But this won't type-check in predicative System F (= Hindley-Milner, HindleyMilner) system:

>>> demo_ emptyCtx $ hindleyMilnerIdentity @@ forall_ "b" ("b" ~> "b") @@@ hindleyMilnerIdentity
error:
• Couldn't match expected type M with actual type P
• In the expression: ∀ b → b → b
• when checking expression
  (λ a x → x : ∀ a → a → a) (∀ b → b → b)
  (λ a x → x : ∀ a → a → a) (∀ b → b → b) (λ a x → x : ∀ a → a → a)

Former is however, ok. Note that we get a polymorphic value!

>>> demo_ emptyCtx $ Ann (lam_ "b" (hindleyMilnerIdentity @@ ("b" ~> "b") @@ (hindleyMilnerIdentity @@ "b"))) (forall_ "b" ("b" ~> "b"))
λ b → (λ a x → x : ∀ a → a → a)
          (b → b) ((λ a x → x : ∀ a → a → a) b)
    : ∀ b → b → b
    ↪ λ b x → x : ∀ b → b → b