[plt-scheme] Typed scheme: Cannot apply expression of type Procedure, since it is not a function type

On Wed, Jun 02, 2010 at 10:32:15PM +0200, keydana at gmx.de wrote:
> 
> > 
> > Notice that our code will type check perfectly but every expression
> > has type Any and these types are essentially useless. This gives you
> > an idea of what static typing does and doesn't check. Basically types
> > are statically checked, but cases (in the discriminated union sense)
> > aren't. Cases are how you inject dynamic checks into statically typed
> > languages. 
> 
> 
> Yes, I think I see what you mean... the discriminated union cases in a way threaten to "dissolve" the type system...
> 
> In fact, it seems to me I'm approaching this from the opposite angle 
> somehow: Taking standard dynamic scheme as the default, I use typed 
> scheme primarily for "educational" purposes - I like being forced to 
> think about how, exactly, the fields of a record (for example) are 
> defined or what exactly a function has to accept/return.
> But even more, I like using the discriminated unions (with the 
> define-datatype macro), they make me think about what "kinds of a 
> thing there are", and they offer an easy way of structuring the code 
> (I'll just have to handle every case and that's it).
> Certainly this also depends on the domain - in my case currently, 
> discriminated unions seem like a very suitable way to implement 
> something "language-like" (the discriminated unions looking like some 
> semantic equivalent of BNF anyway).

Discriminated unions are the category-theoretic dual of cartesian 
products.  If you find one useful, chances are you need the other, too.

>
> On the other hand, they really get inconvenient when there's too much 
> pattern matching to do (speaking of pattern matching, their "natural 
> proneness" to be used with pattern matching - if I my say so - is 
> another reason I like them so much...)
> 
> - All this just from the perspective of a "normal user" (well in the 
> end, I should perhaps also admit that using the algebraic datatypes in 
> typed scheme might be a way of coping with the sad fact that my spare 
> time doesn't  seem sufficient to learn/practice both scheme and 
> haskell :-;)
> 
You might be better off with CAML than Haskell, if you want to make 
smaller steps in that direction.  CAML is not such a radical shift into 
lazy evaluation.

Also, learn some elementary category theory (that found in the first 
chapter or two of *any* book on the subject will be enough to 
familiarize you with the ideas.  The fundamental thing about data types 
is that they form the objects of a category, and the functions between 
them are the arrows.

I believe the Yoneda of Yoneda's lemma is the Yoneda who also worked on 
the design of ALgol 68's tyope system.

-- hendrik