tag:blogger.com,1999:blog-11295132.post114548325935737824..comments2015-11-05T00:40:24.898-08:00Comments on A Neighborhood of Infinity: S4 and Partial EvaluationDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger2125tag:blogger.com,1999:blog-11295132.post-1145911440448464072006-04-24T13:44:00.000-07:002006-04-24T13:44:00.000-07:00Just brainstorming again...Maybe what you're descr...Just brainstorming again...<BR/><BR/>Maybe what you're describing is connected to epistemic logic. In epistemic logic we have a modal operator K where K means "I know that". Instead make K mean "the compiler knows that this is of type...". An object of type Int is an integer, but an object of type KInt is an integer and the compiler knows it at compile time. It's a bit tricky because we're dealing with intuitionistic logic so the standard literature on the subject doesn't all apply.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-1145703754900968622006-04-22T04:02:00.000-07:002006-04-22T04:02:00.000-07:00I had an idea about something similar to this idea...I had an idea about something similar to this idea using a modal logic.<BR/><BR/>If you have a programming language (like twelf) in which you do all computations with proofs about types then you can might be able to use S4 as a type of compile time type checking, mixing dynamic and static typing. <BR/><BR/>As an example let us take a language with a syntax similar to twelf and let us assume we have natural numbers and we want a generic addition.<BR/><BR/>Nat: type. <BR/>z: Nat. <BR/>s: Nat -> Nat. <BR/><BR/>is_nat_z: Nat(z).<BR/>is_nat: Nat(s(X)) <- Nat(X). <BR/><BR/>add_nat: Add(X,Y,Z) <- Nat(X),Nat(Y),Add_nat(X,Y,Z).<BR/><BR/>add_nat_z: Add_Nat(z,Y,Y). <BR/>add_nat_s: Add_Nat(s(X),Y,s(Z)) <- Add(X,Y,Z).<BR/><BR/>Now we pose the query: <BR/><BR/>[](Nat(X),Nat(y),Add(X,Y,Z))<BR/><BR/>We should get the statically typed version of Add_Nat instead of the generic version.Jacobianhttp://www.blogger.com/profile/03650584449231540008noreply@blogger.com