Late Typing in Loosely Coupled Recursion
Late Typing
for Loosely Coupled
Recursion
Ravi Chugh
var tick = function (n) {return n > 0 ? "tick " + tock(n) : "";
};
var tock = function (n) {return "tock " + tick(n-1);
};
tick(2); // "tick tock tick tock "
JavaScript
let (tick,tock) = (ref undef, ref undef)
tick := \n.
n > 0 ? "tick " + !tock n : ""
tock := \n.
"tock " + !tick (n-1)
!tick 2 // "tick tock tick tock "
λ-Calc + Refs
let (tick,tock) = (ref
undef
, ref
undef
)
tick := \n.
n > 0 ? "tick " + !tock n : ""
tock := \n.
"tock " + !tick (n-1)
!tick 2 // "tick tock tick tock "
λ-Calc + Refs
val tick : ref (int -> str)
let tick = ref (\_. "")
val tock : ref (int -> str)
let tock = ref
(\_.
""
)
tick := \n. n > 0 ? "tick " + !tock n : ""
tock := \n. "tock " + !tick (n-1)
!tick 2 // "tick tock tick tock "
λ-Calc + Refs
Simply-Typed
val tick : ref (int -> str)
let tick = ref
(\_. "")
val tock : ref (int -> str)
let tock = ref
(\_. "")
tick := \n. n > 0 ? "tick " + !tock n : ""
tock := \n. "tock " + !tick (n-1)
!tick 2 // "tick tock tick tock "
λ-Calc + Refs
Simply-Typed
(Γ) =>
T -> U
“Open”
Function Types
(Γ) => T -> U
“Open” Function Types
let tick = ref undefined
let tock = ref undefined
val f_tick : (
*tock: int -> str
) => int -> str
let f_tick n = n > 0 ? "tick " + !tock n : ""
val f_tock : (
*tick: int -> str
) => int -> str
let f_tock n = "tock " + !tick (n-1)
tick := f_tick
// Rely: { *tick: int -> str
,
*tock: int -> str
}
// Guar: { *tick: int -> str
, *tock: undefined }
!tick 2
// ill-typed; run-time crash!
let tick = ref undefined
let tock = ref undefined
val f_tick : (
*tock: int -> str
) => int -> str
let f_tick n = n > 0 ? "tick " + !tock n : ""
val f_tock : (
*tick: int -> str
) => int -> str
let f_tock n = "tock " + !tick (n-1)
tick := f_tick
tock := f_tock
// Rely: { *tick: int -> str
,
*tock: int -> str
}
// Guar: { *tick: int -> str
,
*tock: int -> str
}
!tick 2
// well-typed; "tick tock tick tock "
(Γ) => T -> U
“Open” Function Types
“Late” Checking at Calls
let tick this n =
n > 0 ? "tick " + this.tock this n : ""
let tock this n -
"tock " + this.tick this (n-1)
let obj = { tick = tick ; tock = tock }obj.tick obj 2 // "tick tock tick tock "
λ-Calc + Recds
tick : (
ς: {tock: ς->int->str}) => ς -> int ->
str
let tick this n =
n > 0 ? "tick " + this.tock this n : ""
tock : (
ς: {tick: ς->int->str}) => ς -> int ->
str
let tock this n -
"tock " + this.tick this (n-1)
let obj = { tick = tick ; tock = tock }// Rely:
{tick: ς->int->str
,
tock: ς->int->str
}
// Guar:
{tick: ς->int->str
,
tock: ς->int->str
}
obj.tick obj 2 // "tick tock tick tock "
λ-Calc + Recds
(Γ)
=>
T -> U
Late Typing
for Loosely Coupled
Recursion
Explore late typing in loosely coupled recursion through JavaScript and simply-typed calculations. Witness the intricacies of open function types and the guarantee-rely mechanism in defining functions for effective programming.
Uploaded on Sep 28, 2024 | 0 Views
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Late Typing for Loosely Coupled Recursion Ravi Chugh
JavaScript var tick = function (n) { return n > 0 ? "tick " + tock(n) : ""; }; var tock = function (n) { return "tock " + tick(n-1); }; tick(2); // "tick tock tick tock "
-Calc + Refs let (tick,tock) = (ref undef, ref undef) tick := \n. n > 0 ? "tick " + !tock n : "" tock := \n. "tock " + !tick (n-1) !tick 2 // "tick tock tick tock "
-Calc + Refs let (tick,tock) = (ref undef, ref undef) tick := \n. n > 0 ? "tick " + !tock n : "" tock := \n. "tock " + !tick (n-1) !tick 2 // "tick tock tick tock "
Simply-Typed -Calc + Refs val tick : ref (int -> str) let tick = ref (\_. "") val tock : ref (int -> str) let tock = ref (\_. "") tick := \n. n > 0 ? "tick " + !tock n : "" tock := \n. "tock " + !tick (n-1) !tick 2 // "tick tock tick tock "
Simply-Typed -Calc + Refs val tick : ref (int -> str) let tick = ref (\_. "") val tock : ref (int -> str) let tock = ref (\_. "") tick := \n. n > 0 ? "tick " + !tock n : "" tock := \n. "tock " + !tick (n-1) !tick 2 // "tick tock tick tock "
Open Function Types ( ) => T -> U
Open Function Types ( ) => T -> U Guarantee Rely
let tick = ref undefined let tock = ref undefined val f_tick : (*tock: int -> str) => int -> str let f_tick n = n > 0 ? "tick " + !tock n : "" val f_tock : (*tick: int -> str) => int -> str let f_tock n = "tock " + !tick (n-1) tick := f_tick // Rely: { *tick: int -> str , *tock: int -> str } // Guar: { *tick: int -> str , *tock: undefined } !tick 2 // ill-typed; run-time crash!
let tick = ref undefined let tock = ref undefined val f_tick : (*tock: int -> str) => int -> str let f_tick n = n > 0 ? "tick " + !tock n : "" val f_tock : (*tick: int -> str) => int -> str let f_tock n = "tock " + !tick (n-1) tick := f_tick tock := f_tock // Rely: { *tick: int -> str , *tock: int -> str } // Guar: { *tick: int -> str , *tock: int -> str } !tick 2 // well-typed; "tick tock tick tock "
Open Function Types ( ) => T -> U Guarantee Rely Late Checking at Calls
-Calc + Recds let tick this n = n > 0 ? "tick " + this.tock this n : "" let tock this n - "tock " + this.tick this (n-1) let obj = { tick = tick ; tock = tock } obj.tick obj 2 // "tick tock tick tock "
-Calc + Recds tick : ( : {tock: ->int->str}) => -> int -> str let tick this n = n > 0 ? "tick " + this.tock this n : "" tock : ( : {tick: ->int->str}) => -> int -> str let tock this n - "tock " + this.tick this (n-1) let obj = { tick = tick ; tock = tock } // Rely: { tick: ->int->str, tock: ->int->str } // Guar: { tick: ->int->str, tock: ->int->str
Late Typing for Loosely Coupled Recursion ( ) => T -> U
