Term Tracker #1

New issue

Open

opened 2023-11-07 08:43:32 +00:00 by michael · 0 comments

michael commented

2023-11-07 08:43:32 +00:00

Owner

Identity function: \lambda x.x : \forall \alpha.\alpha \rightarrow \alpha
```
>> \x.x
parsed: (λx.x)
synthesized: (∀ π̂* . (π̂* -> π̂*))
```
Identity function applied to unit: (\lambda x.x)\top : \mathbb{1}
```
>> (\x.x) ()
parsed: ((λx.x) · unit)
synthesized: 𝟙
```
K-combinator: \lambda x.(\lambda y.x) : \forall \alpha.(\forall \beta.\alpha \rightarrow (\beta \rightarrow \alpha))
```
>> \x.\y.x
parsed: (λx.(λy.x))
synthesized: (∀ σ̂* . (σ̂* -> (σ̂* -> σ̂*)))
```
This is the wrong type.

- [x] Identity function: $\lambda x.x : \forall \alpha.\alpha \rightarrow \alpha$ ``` >> \x.x parsed: (λx.x) synthesized: (∀ π̂* . (π̂* -> π̂*)) ``` - [x] Identity function applied to unit: $(\lambda x.x)\top : \mathbb{1}$ ``` >> (\x.x) () parsed: ((λx.x) · unit) synthesized: 𝟙 ``` - [ ] K-combinator: $\lambda x.(\lambda y.x) : \forall \alpha.(\forall \beta.\alpha \rightarrow (\beta \rightarrow \alpha))$ ``` >> \x.\y.x parsed: (λx.(λy.x)) synthesized: (∀ σ̂* . (σ̂* -> (σ̂* -> σ̂*))) ``` This is the wrong type.

michael added this to the Term Project project 2023-11-07 08:48:43 +00:00

michael changed title from ~~Project terms~~ to Term Tracker

2023-11-07 08:48:59 +00:00

No labels

No milestone

No project

No assignees

1 participant

Notifications

Due date

The due date is invalid or out of range. Please use the format "yyyy-mm-dd".

No due date set.

Dependencies

No dependencies set.

Reference: school/csci8980-f23#1

No description provided.