Hello Billy,
понедельник, 10 декабря 2001 г., you wrote:
BT> From: Serguey Zefirov [mailto:sz@...]
>>What is more severe than possible functionalitylessness is a fact thatBT> That doesn't make sense to me -- several people have designed static type
>>concatenative languages do not have a type system with principal types
>>(ie, every expression should have _single_ type). This is also true
>>for Linear Logic and is certainly sad.
BT> systems for concatenative languages, although the only one I know of that's
BT> been implemented is strongForth (look it up on Google or talk to the author
BT> on this list). StrongForth isn't perfect, but its principle is, I believe,
BT> good enough to build a type checker which can handle arbitrary code with no
BT> runtime performance hit. (The current version doesn't handle unbalanced
BT> conditionals and loops; I've been working on a system which I believe
BT> could.)
I tried to develop a type notation for applicative languages, based on
the following algebraic rules:
0 - type clash
1 - ( -- )
* - is a table rule
( a -- b c ) ( c -- d) -> ( a -- b d)
( b -- c ) ( a c -- d) -> ( a b -- d)
everything else is 0
a,b,c and d are (maybe empty) sets of stack parameters.
Here EXECUTE (i) has a type:
( alpha ( alpha -- beta) -- beta)
where alpha and beta are lists of stack parameters.
I tried my best to calculate type for concatenated EXECUTE's and
failed to obtain a single expression type signature.
(BTW, I've done several posts about it here a year or so ago)
Maybe you succeed.
>>To exemplify that I invite you (and everyone other in the list) toBT> I, in turn, invite you to calulate the type of the expression i(i), as
>>calculate type for expression
>>i i
BT> expressed in an applicative language. To match your challenge, I'm not
BT> telling you which applicative language, nor giving you any declarations for
BT> i. Since I called it an "expression", though, you know for sure it's not
BT> Lisp and probably not Fortran, so you have one hint I don't have.
I thought that i is a combinator that resembles EXECUTE word in Forth.
I was in some hurry writing this. Well, show me type signature for Forth's
EXECUTE EXECUTE
in any type notation for concatenative languages you wish. I think
that it will contain several different signatures due to the lack of
principal type.
Then we going to applicative language.
i(i)
i is a function (a -> b). Since it is applied to function (a -> b)
it's signature ( c -> b, c == a -> b), or (a -> b -> b). Repeating
substitution further we found that we dive into endless recursion and
hugs (a Haskell implementation) tells us about it.
BT> In other words, I don't think you've given enough information; and I think
BT> that's true for your question in ANY language.
Well, not. ;) In applicative languages it just does not allowed.
>>'i i' has a bunch of possible types, and their number depends on howBT> How could it? In a concatenative language there are no arguments.
>>we differe lists of arguments (in my understanding of this).
Oops, there are. putchar should have char on top of stack to output
it. There is one argument (stack) but it is just inconvenient to view
it without details. There are arguments, otherwise type system is
irrelevant.
>>This somewhat prevents one from reasoning about programs, especially,BT> As I've mentioned, several people have designed static type systems;
>>their parts.
BT> additionally, programmers have been reasoning about Forth programs for three
BT> decades.
Let's read - "makes it harder to reason about..." When I get
thirty-two different type expressions for innocent line I get stuck
for sure. It is joke but not without sense.
Best regards,
Serguey Zefirov mailto:sz@...
Hello Louis,
вторник, 11 декабря 2001 г., you wrote:
LM> On Monday, December 10, 2001, at 11:37 PM, Serguey Zefirov wrote:
>> What is more severe than possible functionalitylessness is a fact thatLM> Joy doesn't have a type notation, so I'll invent one quickly: [t] means
>> concatenative languages do not have a type system with principal types
>> (ie, every expression should have _single_ type). This is also true
>> for Linear Logic and is certainly sad.
>>
>> To exemplify that I invite you (and everyone other in the list) to
>> calculate type for expression
>>
>> i i
>>
LM> a quoted type for some arbitrary type t, [[t]] means double quoted and
LM> this is indeed the type required by ii. Many kinds of values have the
LM> type [[t]] including for example [[3]] and [[4 +] 3 cons]
This is just a part of type signature. One single line. It does not
mention relationship between input stack, output stack and stack on
entry of enclosed quotation.
>> 'i i' has a bunch of possible types, and their number depends on howLM> If you're getting multiple types for some expression, then that is more
>> we differe lists of arguments (in my understanding of this).
>>
LM> an artifact of the type system you've chosen rather than the language
LM> itself.
LM> As an extreme example, I can state that all programs in any language
have the type "a ->> b" where a is some arbitrary input and b is some
LM> derived output. From this, I can conclude that all languages have
LM> principle types.
This is very reasonable, I agree, but simplistic to no-use. As no-use
as "concatenative programs have no parameters".
LM> Languages like Clean and Haskell do have decidable type systems but only
LM> because their language designers chose to limit the expressiveness of
LM> the underlying untyped language. For example, if the type system didn't
LM> get in the way, you would be able to define a 'printf' type function
LM> where the types of the second and subsequent arguments are determined by
LM> the first argument.
BTW, so called existential types handle this as well without
sacrificing decidability.
LM> If you wanted to, you could similarly limit Joys expressiveness and so
LM> define a decidable type system for it, but I dislike that approach.
Well, I'd like to see your approach.
Best regards,
Serguey Zefirov mailto:sz@...
On Tuesday, December 11, 2001, at 09:45 PM, Serguey Zefirov wrote:
> Hello Louis,Hello Serguey,
>Well the full signature would be [[t]] -> t
> вторник, 11 декабря 2001 г., you wrote:
>>> To exemplify that I invite you (and everyone other in the list) to
>>> calculate type for expression
>>>
>>> i i
>>>
>
> LM> Joy doesn't have a type notation, so I'll invent one quickly: [t]
> means
> LM> a quoted type for some arbitrary type t, [[t]] means double quoted
> and
> LM> this is indeed the type required by ii. Many kinds of values have
> the
> LM> type [[t]] including for example [[3]] and [[4 +] 3 cons]
>
> This is just a part of type signature. One single line. It does not
> mention relationship between input stack, output stack and stack on
> entry of enclosed quotation.
Though I have no idea what you mean by "stack on entry of enclosed
quotation".
>Hmmm, really? Can you show me?
> LM> Languages like Clean and Haskell do have decidable type systems but
> only
> LM> because their language designers chose to limit the expressiveness
> of
> LM> the underlying untyped language. For example, if the type system
> didn't
> LM> get in the way, you would be able to define a 'printf' type function
> LM> where the types of the second and subsequent arguments are
> determined by
> LM> the first argument.
>
> BTW, so called existential types handle this as well without
> sacrificing decidability.
>I'm working on it :-)
> LM> If you wanted to, you could similarly limit Joys expressiveness and
> so
> LM> define a decidable type system for it, but I dislike that approach.
>
> Well, I'd like to see your approach.
Louis.
[Non-text portions of this message have been removed]