Hello Louis,
>>
>> 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.
LM> Well the full signature would be [[t]] -> t
LM> Though I have no idea what you mean by "stack on entry of enclosed
LM> quotation".
i takes a quotation from top of stack and unquotes it. By unquoting we
understand concatenation of effects. So, let's see:
[[1]] i i === 1
2 [drop [1]] i i === 1
-1 4 [+ 2 [-]] i i === 1
1 [ ] 'a' [ putchar ] i i === 1
1 'a' [ putchar ] [ ] i i === 1
......
First (level of) quotation may have any number of concatenative
effects, even side effects, everything we need is that we should have
a quotation on top of stack a the end.
So what type will have quotation [drop 3 + [-]] in your notation?
>>
>> 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> Hmmm, really? Can you show me?
------------------------------------------
-- Type T could carry any value that is showable.
-- So it is very specialized to printf-like funcs.
-- I can create a list of T's, where every T will carry value of
-- different type. I didn't explore that field well, but
-- sufficient to make an example.
data T = forall a . Show a => T a
a (T x) (T y) (T z) = "This simple function will show you (in order of appearance):\n"++
"x : "++show x++"\n"++
"y : "++show y++"\n"++
"z : "++show z++"\n"
testa = putStrLn $ a (T "Wow! x!") (T 10) (T $ Just "I am Z")
------------------------------------------
It works with hugs 98. Save text between dashes into file a.hs, then
run "hugs -98 a.hs", then type "testa <ENTER>".
BTW, I cannot use expression from pattern (T a) except for calling
show function. So expression like
data U = forall a . U a
is completely meaningless (we do not provide any mean to manipulate
with a), but perfectly legal.
I've learned about existential types a year ago when someone explained
his Joy in Haskell thoughts. ;)
Best regards,
Serguey Zefirov mailto:
sz@...