Opened 7 years ago

Closed 3 years ago

#290 closed defect (fixed)

Evaluator doesn't preserve closure typing.

Reported by: benl Owned by:
Priority: normal Milestone: 0.5.0
Component: Core Type Checker Version: 0.2.1
Keywords: Cc:

Description

Typing L1# doesn't reveal the Use R1# closure term.

Change History (7)

comment:1 Changed 7 years ago by benl

  • Milestone changed from 0.3.0 to 0.4.0

In the semantics, the closure of a location should be all the regions reachable from that location, but we don't have a way of doing this in the current implementation of the type checker. The type checker is polymorphic in the name type, and doesn't distinguish between locations and other constructors.

        L1# : (T, C) \in SE
-------------------------------------
 KE | TE | SE |- L1# :: T ; !0 ; C

To make tagged closures work the store environment needs to contain the tagged closure of each location, as well as its type. The store environment will contain an upper bound on the reachability graph of the store, but abstract away from the actual values contained within.

To implement this we'll probably need to add a proper store typing to the type checker, instead of attaching just the type of each location directly to the location constructors.

Last edited 7 years ago by benl (previous) (diff)

comment:2 Changed 7 years ago by benl

  • Milestone changed from 0.4.0 to none

comment:3 Changed 7 years ago by benl

To invoke the bug, re-enable the code that checks closure typing is preserved after each evaluation step. In DDCI.Core.Command.Eval.

comment:4 Changed 7 years ago by benl

  • Milestone changed from none to 0.4.0

comment:5 Changed 5 years ago by benl

  • Milestone changed from 0.4.0 to 0.5.0

comment:6 Changed 3 years ago by benl

Closure typing is no longer part of the Tetra language, and we removed it from core.

comment:7 Changed 3 years ago by benl

  • Resolution set to fixed
  • Status changed from new to closed
Note: See TracTickets for help on using tickets.