Talk:%thaw

From The Twelf Project
Jump to: navigation, search

Gee that's bad

ARGH! The current Twelf CVS allows you to

nat : type.
s : nat -> nat.
z : nat.

plus : nat -> nat -> nat -> type.
p-z : plus z N N.
p-s : plus (s N1) N2 (s N3) <- plus N1 N2 N3.

%mode plus +A +B -C.
%worlds () (plus _ _ _).
%total T (plus T _ _).

Take 1:

fake : nat.
%solve _ : plus fake z _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

fake : nat. %solve plus fake z X1. Error: No solution to %solve found

%% ABORT %%

Take 2:

%thaw nat.
fake : nat.
%solve _ : plus fake z _.
Twelf 1.7.1+ (r1896, built 05/05/15 at 12:56:43 on yazoo.plparty.org)

%thaw nat. fake : nat. %solve plus fake z X1. Error: No solution to %solve found

%% ABORT %%

argh. — Rob (and his talk) 22:06, 29 December 2006 (EST)

Fixing this is a three-line patch to Twelf, but because it would break potential existing code I've asked Frank for permission to commit the patch — Rob (and his talk) 22:25, 29 December 2006 (EST)
How would it break existing code? My feeling is that %thaw should pretty much be removed from the language. It doesn't seem to have any legitimate use to me (unlike say %trustme).  — Tom 7 10:18, 28 February 2007 (EST)
See /twelf/examples/lp/test.cfg for the only significant code I broke banning Thaw. If you've frozen your language of atoms and you now need more atoms, you can declare them dynamically, which is an enormous mess in this example, or you can just thaw your base atom type knowing you're justified by the way you wrote all your %block and %worlds directives. — Rob (and his talk) 12:49, 28 February 2007 (EST)
OK, I buy that use. I'm not sure it's really an enormous mess to introduce them dynamically, but that is certainly clean to do it this way. On the other hand, maybe I should never defend a use of unsafe features that's not clearly necessary?  — Tom 7 14:26, 28 February 2007 (EST)
I also would say that we shouldn't advocate it's use so much, but there's a code compatibility issue; perfectly legitimate code written before autofreeze, in particular, may need extensive rewriting, whereas if that code is not crucial it's a decent hack to just thaw things. — Rob (and his talk) 15:13, 28 February 2007 (EST)
Agreed—I meant specifically me in that will I be able to sleep well at night if I support that? ;)  — Tom 7 16:27, 28 February 2007 (EST)