search

nigelflower / LambdaCalculator-Issues

pedagogical tool for students of natural language semantics
http://lambdacalculator.com/
0 stars 0 forks source link

Product types #9

Open nigelflower opened 3 years ago

nigelflower commented 3 years ago

created by mattghg on Aug 15, 2016

Hi,

I note that product types are implemented in the Lambda Calculator to an extent. I have three requests about ways in which the implementation could be extended, working (presumably) from the simplest to the most complicated.

1) When an expression of product type is the argument to a function, things don't work as expected - type inference doesn't work, which causes the derivation to crash if you go any higher up in the tree:

test-var not-test-var first-var second-var

The minimal working example that produced these results is here:

MWE.txt

2) It's not possible to define nested product types, e.g. e X (e X v). I know that it is possible to define e X e X v, but for my purposes those are different (I also want to use (e X e) X v, for example).

3) You can see from the MWE that I'm trying to make use of term constructors and destructors for product types. It would be super if they could be implemented along with their accompanying beta reduction inference patterns.

nigelflower commented 3 years ago

alexwarstadt commented on Sep 3, 2018

Parts 1 and 2 of this issue have been addressed.

nigelflower commented 3 years ago

alexwarstadt commented on Sep 3, 2018

Part 3 is a feature request which requires additional, more extensive changes.