Re: Typed Guile?

[Panicz Maciej Godek]

2012/11/8 Ian Price <address@hidden>:
>> I've heard a lot about the type system of Haskell, but I don't know
>> any details. Neither do I know much about racket's, but I know for
>> sure that it doesn't suit my taste.
> How can you accurately judge something you don't know much about?

Because it's my taste that I'm judging, and on this I'm the expert :)
(Obviously, I did a tiny research before responding to the e-mail,
but as a language the TR system seemed too far away from scheme
and too complex syntactically and lexically. Perhaps it's just the appearance,
semantically meaningless, to be pleonastic, but I find the aesthetic part
of programmer's experience quite significant)

>> GOOPS' type system is lacking two features, the first one being the
>> return value of a procedure, and the second, types for collections.
>>
>> So I think, that type annotation for the return value of a method
>> could be a coherent extension to the existing system. For example, one
>> could write:
>> (define-method (name (arg1 <type1>) ... (argN <typeN>)) : <return-type>
>>   body ...)
>> slightly extending the define-method as it is used today.
> Adding syntax for this is easy, but it would completely change the
> nature of Scheme. How does a procedure know which type to return?

I think I see the point. This is indeed a good question, and an
interesting task,
but initially it could be implemented only partially (we just check whether
the declared argument types match, so for instance if we had a
((p1 <type1>) : <type2>) and (p2 <type2>), and then we could typecheck
that (p2 (p1 x)) is OK at least in terms of declaration, and we could
additionally issue runtime warnings if the actual return type didn't match
the intended one).
More sophisticated type inference could be developed later, and the
type system could prove useful even without it.
And I don't know what you mean when you say about "changing
the nature of Scheme". I think it's understood that the type system
is completely optional.

> It can either infer it, which requires more than a simple extension of
> goops, or you can return some sort of "value", than you then tell which
> type you expect it to have. Which may mess with the order of
> evaluation (I'd more time to think about this), and wouldn't play well
> with non-goops procedures.

I'm not sure if I read you right, but perhaps it would be enough to
implement type system for goops procedures only. And I think that type
checking could be a separate stage, independent from compilation or
evaluation -- but that's mainly because I don't know much about
guile's evaluator nor compiler.

[...]
>> It could be similarly used to define methods with variable number of
>> arguments of the same type, e.g.
>> (define-method (mean (n <number>) . (rest (<number> ...))) : <number>
>>   (mean (cons n rest)))
>
> This will not work with arbitrary user defined collections?

I'd need to see an example. (As I remarked, my main intent in having a
type system is to make the code clearer). I can't even imagine how
does one define a collection in Scheme.
But I agree that the notation that I proposed has some serious
deficiencies. For instance, how to mark the type of a procedure that
takes whatever arguments, and returns a strict type?
((procedure . args) : <type>)?
((procedure . <top>) : <type>)?
Is it ok that this specification is a nested list?

>> I don't know what the rest of the community has to say about this, but
>> if you managed to implement this, I can promise that you'd have at
>> least one user :)
>
> Unless you give me more details about how this is to work, I think an
> implementation is out of the question.

As I said, initially it could be a stage separate from compilation and
evaluation.
I even think that the type inference wouldn't need to be so
complicated, because there are strict rules regarding which value is
the value of expression. If it's a conditional, we just check return
values of both branches. If it's a call/cc, we check all the calls of
its argument's argument, and so on, ad finitum :)
Obviously, some compiler optimizations regarding the types could be
added with the time, but for now I don't consider them crucial.
That's how I see it, more or less.

>> BTW Does anyone here know what does the #& ("box") quasi-pattern in
>> the Shinn-Wright pattern matcher stand for?
> A box is, more or less, a one element vector. Guile does not have a box
> type, nor reader syntax for it, arguably it should...

Thanks a lot :)
MG