splintah / old-site Goto Github PK

You have a minor typo on the page:
https://splintah.github.io/posts/2020-05-24-Simply-typed-lambda.html

you should change t to tx:

`
case typeOf ctx' t of
Left e -> Left e
Right ty' -> Right (TyFun ty ty')

to

case typeOf ctx' ty of
----------------------^^
Left e -> Left e
Right ty' -> Right (TyFun ty ty')
`

Best wishes,
Henry Laxen

I hope you don't mind if I ask you a question.
On your page at:
https://splintah.github.io/posts/2020-05-27-Polymorphic-lambda.html

you define:

type of const : \/ A. \/ B. A -> B -> A
Further down the page you say: "The first step is:"

then in your definition of T-TyApp you have:

in context Gamma we know : type of const : \/ A. \/ B. A -> B -> B
------------------------------------------------------------------
in context Gamma we know : type of const B : (\/ B. A -> B -> A)[A:=B]

Now I'm confused. Don't you mean?

in context Gamma we know : type of constFlip : \/ A. \/ B. B -> A -> B
------------------------------------------------------------------
in context Gamma we know : type of constFlip B : (\/ B. B -> A -> B)[A:=B]

you still get: subst gives: \/ B. B -> B -> B

or do you mean?

in context Gamma we know : type of const : \/ A. \/ B. A -> B -> A
------------------------------------------------------------------
in context Gamma we know : type of const B : (\/ B. A -> B -> A)[A:=B]

and you still get: subst gives: \/ B. B -> B -> B

I don't see how

const : \/ A. \/ B. A -> B -> B
became
const B : (\/ B. A -> B -> A)[A:=B]

By the way, I'm really enjoying reading your posts about types. This
is really the first time I think I understand why Haskell has those
implicit foralls everywhere. Thanks so much for taking the time to
write this.

Best wishes,
Henry Laxen