Hello e1_t,
суббота, 8 декабря 2001 г., you wrote:
e> That reasoning could also be used for impure functional languages and
e> in fact imperative languages as well.
e> What happens if you write a function that uses 'get'? Does that
e> function also take a hidden argument (afterall it does cause a side-
e> effect)? How does the compiler/interpreter know which function takes
e> hidden arguments and which one doesn't?
In a current state Joy isn't pure functional. This can be fixed by a
simple hack - introduce a type World.
getsome ( World -- World something)
If you protect type World from being duplicated and dropped, you get a
pure functional language, like, say, Concurrent Clean.
I've not thought yet the way that could be done with something like
Haskell Monads.
e> The question of whether the compiler needs to know that is in fact
e> relevant - functional languages are viewed as better then imperative
e> languages simply because they can be implemented to utilize
e> equational reasoning (which can ultimatly be used to optimize an
e> abstract and inefficient program that is easily readable by a human,
e> i.e. a math formula, into an efficient form that may be harder to
e> comprehend) and because they are better suited to parallel
e> programming (the order of evaluation of pure, side-effect free
e> functions is irrelevant therefore they can be executed in parallel).
e> One of my current projects is Metafor, a functional language based on
e> Forth that can be implemented as an extension to Forth. I was
e> surprised when I came accross Joy as the syntax is very similar. I'm
e> still designing Metafor and haven't even started implementing it yet
e> simply because I'm still evaluating the potential flaws and one of
e> the biggest is the way side-effects are handled in the current
e> design. In fact I was hoping someone would respond the way you did
e> because my reasoning behind hiding side-effects in Metafor is similar
e> (although goes into more detail).
What is more severe than possible functionalitylessness is a fact that
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
'i i' has a bunch of possible types, and their number depends on how
we differe lists of arguments (in my understanding of this).
This somewhat prevents one from reasoning about programs, especially,
their parts.
Best regards,
Serguey Zefirov mailto:sz@...
From: Serguey Zefirov [mailto:sz@...]
>What is more severe than possible functionalitylessness is a fact thatThat 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.
systems for concatenative languages, although the only one I know of that's
been implemented is strongForth (look it up on Google or talk to the author
on this list). StrongForth isn't perfect, but its principle is, I believe,
good enough to build a type checker which can handle arbitrary code with no
runtime performance hit. (The current version doesn't handle unbalanced
conditionals and loops; I've been working on a system which I believe
could.)
>To exemplify that I invite you (and everyone other in the list) toI, in turn, invite you to calulate the type of the expression i(i), as
>calculate type for expression
>i i
expressed in an applicative language. To match your challenge, I'm not
telling you which applicative language, nor giving you any declarations for
i. Since I called it an "expression", though, you know for sure it's not
Lisp and probably not Fortran, so you have one hint I don't have.
In other words, I don't think you've given enough information; and I think
that's true for your question in ANY language.
>'i i' has a bunch of possible types, and their number depends on howHow could it? In a concatenative language there are no arguments.
>we differe lists of arguments (in my understanding of this).
>This somewhat prevents one from reasoning about programs, especially,As I've mentioned, several people have designed static type systems;
>their parts.
additionally, programmers have been reasoning about Forth programs for three
decades.
>Serguey Zefirov mailto:sz@...-Billy
On Monday, December 10, 2001, at 11:37 PM, Serguey Zefirov wrote:
> What is more severe than possible functionalitylessness is a fact thatJoy 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
>
a quoted type for some arbitrary type t, [[t]] means double quoted and
this is indeed the type required by ii. Many kinds of values have the
type [[t]] including for example [[3]] and [[4 +] 3 cons]
> 'i i' has a bunch of possible types, and their number depends on howIf you're getting multiple types for some expression, then that is more
> we differe lists of arguments (in my understanding of this).
>
an artifact of the type system you've chosen rather than the language
itself.
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
derived output. From this, I can conclude that all languages have
principle types.
The hard part in designing a type system however, is to get it to
guarantee that one or more formal properties will hold for all
well-typed programs (eg. "no execution can result in an operation being
applied to a value it is not intended to handle", "no array accesses
will be out of bounds", etc). Within these constraints, you could argue
that some type systems (not languages!) don't produce principle types -
this is essentially the same as saying those type systems are
undecidable.
Kris De Volder has written an interesting thesis called "Type Oriented
Logic Programs"[*] in which he questions the obsession that many
language designers have with keeping their type systems decidable.
Here's a quote from his introduction:
"We will show that undecidability and ambiguity of type systems is not
by definition
a bad thing. Ensuring unambiguity and decidability of typing imposes
strong restrictions on
the expressiveness of the type system. When abandoning the restrictions,
the expressiveness
of the type system can be increased to the level of a real programming
language, thus lifting
its capability for active manipulation of static types to an entirely
new level. We will show
by means of examples that this extra expressiveness does have very
useful and interesting
applications."
Languages like Clean and Haskell do have decidable type systems but only
because their language designers chose to limit the expressiveness of
the underlying untyped language. For example, if the type system didn't
get in the way, you would be able to define a 'printf' type function
where the types of the second and subsequent arguments are determined by
the first argument.
If you wanted to, you could similarly limit Joys expressiveness and so
define a decidable type system for it, but I dislike that approach.
> This somewhat prevents one from reasoning about programs, especially,I really have to disagree.
> their parts.
Louis.
{*] "Type Oriented Logic Programs"
Kris De Volder
http://www.cs.ubc.ca/~kdvolder/publications/phd-summary.htm
[Non-text portions of this message have been removed]