K-user mailing list

["Seyed H. HAERI (Hossein)" <hossein.haeri AT gmail.com>]

... My apologies: I posted the wrong link for the paper I referred to. Here is the right one:

[1] http://www.plancomps.org/funkons-component-based-semantics-in-k/

On 29 April 2014 13:19, Seyed H. HAERI (Hossein) <hossein.haeri AT gmail.com> wrote:

Dear all,

Consider the following snippet from [1]:

syntax K ::= "reset-env" "(" Map "," K ")" [strict(2)]

I wonder whether the sort "K" above is like "Object" of Java (and "Any" of Scala)? Or, is it like a type parameter with statically checked properties? [1] explains the above snippet as: "The K argument could be of sort Expr, Decl or Comm." I understand that with the open-endedness assumption, the user of "reset-env" is allowed to include other sorts in their PL and kompile will handle that appropriately. Yet, as a "reset-env" user, will kompile stop me if I assign to K valid Funkon sorts that I haven't included in my very PL? Personally, if the answer is yes, I would say K is a "sort parameter". Otherwise, I would say it's like the common numb types of PLs such as Object or Any.

I have the impression that the difference between the two categories is obvious to most list members. But, for those of us who might not be sure, the P.S. should hopefully make things clear.

TIA,

--Hossein

[1] http://www.plancomps.org/bachpoulsen2014a/

P.S.

Consider the following Scala snippet:

scala> val a: Any = 2;
a: Any = 2

scala> val b: Any = "two";
b: Any = two

In many PLs, there are types like "Any" which do not carry any information about their value. For example, neither does "a" above know that it's carrying an integral value, nor does "b" know that it's carrying a string. As such, no meaningful operation can be performed on either variable (except via runtime casting). Yet, the type "Any" is useful in that it can take values of all types. And, that flexibility can sometimes come handy.

In contrast, type parameters are also common in PLs. They are also flexible in that one can substitute different types for them. Yet, they assist the type system by the valuable static information they provide about the values they take. For example, the Scala code below tells the compiler (statically) that the function "f" returns a value of the same type as its parameter:

def id[T](x: T): T = ...

As such, the type system will stop an attempt to return value of other types than T.

--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------

--
--------------------------------------------------------------------------------------------------------------

Seyed H. HAERI (Hossein)

Research Assistant
Institute for Software Systems (STS)
Technical University of Hamburg (TUHH)
Hamburg, Germany

ACCU - Professionalism in programming - http://www.accu.org/
--------------------------------------------------------------------------------------------------------------