Re: [Chicken-users] permissive checking of sum types

[David Goffredo]

Thank you for your helpful response, Peter.

I will be mindful of Chicken's dynamic nature when using the type 
system. But as you said, declared types are gospel. I would expect that 
means when I write:

    (: foo (or string false))

I'm declaring that the name "foo" shall have the type that is the union 
of the strings and #f, regardless of the reality at runtime. Then, when 
I further declare that:

    (: printed (string -> string))

I'm saying that the name "printed" shall have the type of a function 
taking one string argument and returning a string. This is regardless of 
the type of the runtime value of printed's arguments, or even the 
definition of printed itself.

So my question is why the compiler doesn't warn on:

    (printed foo)

when it can be determined statically that the argument has (rather -- is 
declared to have) an incompatible type. Maybe the types will be 
compatible at runtime and maybe not, but as declared they are 
incompatible, in my opinion.

Another way I might ask the question is this: why does example 5' emit a 
warning when example 4' does not?

    ; Example 4' (no warning)
    (: value4 (or string false))
    (printed value4)

    ; Example 5' (warning)
    (: value5 (or number false))
    (printed value5)

Note the lack of definitions, since here I'm concerned only with the 
declared types.

Regards,
    David

On 12/03/2017 06:04 AM, Peter Bex wrote:
> On Sat, Dec 02, 2017 at 08:56:52PM -0500, David Goffredo wrote:
> > Hello everyone,
> >
> > I've been playing around with Chicken for about a month now, and so far
> > really enjoy it. Even got it building and (mostly) working on crusty old AIX
> > and Solaris machines.
> Hi David,
>
> Cool!  That's very good to hear.
>
> > I'm new to Scheme in general. My current project will involve some record
> > types, and I'd like to use Chicken's type information as documentation and
> > to catch simple programming mistakes.
> Please be mindful that CHICKEN's type system accepts declared types as
> gospel, which means you may run into issues when the types don't match
> the declared types.  In other words, procedures should always check their
> argument types.
>
> > This is where I noticed something. I can compile, without producing any
> > warnings, a program that passes a variable declared as "(or T U)" (where "U"
> > and "T" are different) as an argument to a function whose argument at that
> > position is declared as "T". I feel like this should be a type violation,
> > since the input value could be a "T" or a "U", which is not a "T".
> >
> > Is this a bug that I should look into fixing, or do I misunderstand the type
> > system? Or maybe I'm wrong for some other reason.
> The reason this will not produce a warning is that Scheme is not purely
> functional; you can always set!  a variable to a new value which might
> have a different type, and you don't want procedures to be specialised
> incorrectly for the type of the "current value", as the type may change
> later.
>
> >     ; Example 4 (!)
> >     (: value4 (or string false))
> >     (define value4 #f)
> >     (printed value4)
> (set! value4 "hi")
> (printed value4)
>
> The same goes for using fluid-let to temporarily rebind a variable
> to a new value: this should be possible at any time.
>
> I hope this clarifies things a bit.  I'm not the most knowledgeable
> person when it comes to type systems, so if anyone wants to correct
> me on any specific points, please do!
>
> Cheers,
> Peter