# Re[6]: [stack] Joy, purely functional?

## Serguey Zefirov — 2001-12-11 14:23:41

    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@...

## Louis Madon — 2001-12-11 21:58:18

    Hi Serguey,

     On Wednesday, December 12, 2001, at 12:23  AM, Serguey Zefirov wrote:

    >

    > So what type will have quotation [drop 3 + [-]] in your notation?

    >

    its still [[t]].  Its a very abstract notation that ignores lots of

    details.  It wouldn't be useful for  what is normally considered type

    checking.

    > ------------------------------------------

    > -- 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>".

    Well ok, but this is not what I had in mind. 'printf' requires a format

    string, eg: "read %d bytes from %s" and we want to ensure that the

    programmer is passing the right types of subsequent arguments to match

    up with it (an integer and string in this case). The approach you

    describe would allow the wrong types to be passed.

    Notice that with existential types there is no way to check the

    relationship between the format argument and the subsequent arguments

    even at runtime (so while the type system remains decidable, it is only

    type checking the program in a loose sense).

    Louis.

    [Non-text portions of this message have been removed]