search

AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Simplify ugly recursive type #234

Closed AshleyYakeley closed 8 months ago

AshleyYakeley commented 10 months ago

rec a, (rec b, Maybe. (rec c, b | Maybe. c)) | Maybe. a

I believe this is equivalent to rec a, Maybe a.

AshleyYakeley commented 10 months ago

Subterm: rec b, Maybe. (rec c, b | Maybe. c)

AshleyYakeley commented 9 months ago

Can do this reduction:

rec b, Maybe (rec c, b | Maybe c)
⇒ 
b = Maybe c
c = b | Maybe c
⇒ 
b = Maybe c
c = Maybe c | Maybe c
⇒ 
rec b, Maybe (rec c, Maybe c | Maybe c)
⇒ 
Maybe (rec c, Maybe c | Maybe c)

Gets as far as:

rec a, (rec b, Maybe (rec c, b | Maybe c)) | Maybe a
⇒
rec a, (Maybe (rec c, Maybe c | Maybe c)) | Maybe a
⇒ 
rec a, (Maybe (rec c, Maybe c)) | Maybe a
⇒ 
rec a, ((rec c, Maybe c) | Maybe a)
AshleyYakeley commented 9 months ago

Converting to type automata will solve this, per Dolan sec. 7.1.2.

AshleyYakeley commented 8 months ago

Fixed.