search

hazelgrove / HZ

Simple reference implementation of Hazelnut using js_of_ocaml and OCaml React. (frozen -- ongoing development in the hazel repo)
http://hazel.org/HZ/hz.html
MIT License
29 stars 3 forks source link

numeric literal consistency on acceptable values #29

Closed ivoysey closed 8 years ago

ivoysey commented 8 years ago

in the paper we don't really specify what implements num. in the agda, it's Nat. in the implementation we ban decimals but not negatives.

cyrus- commented 8 years ago

is it possible to just treat it abstractly in the agda?

ivoysey commented 8 years ago

yes, but it's messy. just to get the theorems to go through you do need to know that equality is decidable for whatever the literals are. to consider a dynamics, you also want to know that there's something like addition. so you'd want to abstract over a ring-structure with decidable equality for the members.

i (we?) chose not to do this for the POPL paper because it clutters up the proofs a fair amount -- everything everywhere would need to be abstract over this equality. it's a fairly common practice to use Nat as a stand in for "something with decidable equality that we don't really care about".

---Ian

On 10 October 2016 at 12:13, Cyrus Omar notifications@github.com wrote:

is it possible to just treat it abstractly in the agda?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/29#issuecomment-252667929, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIFO5dUJS4lnU5E1X9kdSfc-HRtAiks5qymQRgaJpZM4KSsKF .

cyrus- commented 8 years ago

ok, well banning negatives should be pretty straightforward if you prefer but right now the implementation also bans numbers outside the range of OCaml integers...

cyrus- commented 8 years ago

this is probably something we can just note under "representation decisions" in both READMEs rather than trying to make them match, since the "spec" kinda left the details of "num" to each implementation

ivoysey commented 8 years ago

And the Agda bans numbers that, in unary, induce a larger machine representation inside Agda than the amount of RAM you happen to have. :)

I feel like it's nice to have consistency between the tools, anyway. The paper doesn't specify, Nat is kind of the thing that lets us emphasize the right thing in Agda, so maybe Nat here too?

In either case, I'll add a comment to the README.md for the mechanization about why it's Nat so that it's more clear there.

---Ian

On 10 October 2016 at 12:16, Cyrus Omar notifications@github.com wrote:

ok, well banning negatives should be pretty straightforward if you prefer but right now the implementation also bans numbers outside the range of OCaml integers...

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/29#issuecomment-252668783, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIIHsvDHdoIJnvipx13IsEiybCF3yks5qymTtgaJpZM4KSsKF .

cyrus- commented 8 years ago

using actual unary nat in the OCaml is a bunch of boilerplate code (to parse numerals to nats etc.) I don't feel like writing, and the size of the model then grows with the numbers themselves. so I'm just going to note that we use OCaml integers for num in the README

ivoysey commented 8 years ago

I'm definitely not proposing that the implementation shouldn't use 32-bit integers. My concern is that there are things that you can do in the implementation that you cannot do in Agda. So you can construct the Figure 1 example that adds -5 instead of 1 in HZ but there is no derivation for that given by constructability.

---Ian

On 10 October 2016 at 12:21, Cyrus Omar notifications@github.com wrote:

using actual unary nat in the OCaml is a bunch of boilerplate code (to parse numerals to nats etc.) I don't feel like writing, and the size of the model then grows with the numbers themselves. so I'm just going to note that we use OCaml integers for num in the README

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/29#issuecomment-252669940, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIBPFVH3dzKZL_40X729bcLjbreiHks5qymYKgaJpZM4KSsKF .

cyrus- commented 8 years ago

OK maybe the best thing is to ban negative numbers and then point out the impl has a lower ceiling than "max memory"?

ivoysey commented 8 years ago

That sounds good.

---Ian

On 10 October 2016 at 12:39, Cyrus Omar notifications@github.com wrote:

OK maybe the best thing is to ban negative numbers and then point out the impl has a lower ceiling than "max memory"?

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/hazelgrove/HZ/issues/29#issuecomment-252674236, or mute the thread https://github.com/notifications/unsubscribe-auth/AD6MIIq7p6oJVN2JxSQ8BgYHAZMggvVuks5qymovgaJpZM4KSsKF .