Can not derive type for id id

hexresearch / hschain-utxo

UTXO-based contracts for hschain

0 stars 0 forks source link

Closed anton-k closed 3 years ago

anton-k commented 3 years ago

This program fails with type-check error

x = id
y = id

main = x y

anton-k commented 3 years ago

Thouqh it can derive type for expression id id in the repl

Shimuuar commented 3 years ago

I think it's because

id = λa. a
x = id
y = id
main = x y

Is not typable in simply typed λ-calculus.