[racket] Contract for methods with optional arguments

On Aug 31, 2013, at 2:19 PM, Diego Sevilla Ruiz wrote:

> The example you give for C, you're right, it is not appropriate for C because C has a (lax) static type system.

Let's call it what it is: unsound. Let's also agree that C's type system is so impoverished that it is simply useless to talk about in such contexts. 


> You know, Scheme, Racket, they are dynamically typed languages: the type of the elements can vary at run time, so there are a lot of situations in which the type itself of the element changes.

Racket's values cannot change 'type' at run-time. In principle, we shouldn't use the word 'type' for dynamic concepts -- types are a static discipline -- but when you are given a value, any predicate you apply to it will always return the same answer over the course of the entire execution. 


> The Racket API is full of this. Take into account for example object-info:
> 
> http://docs.racket-lang.org/reference/objectutils.html?q=object-info#%28def._%28%28lib._racket%2Fprivate%2Fclass-internal..rkt%29._object-info%29%29
> 
> It returns either a class or #f. Clearly, these are two different types, and even in this case, it depends on some inner property of the class and the environment (the inspector). In my case, the return type depends on some argument, and I think this also is a pattern that appears in these dynamic languages.

What you mean to say is that functions can return sum 'types' and with case contracts you can even specify when a type is desired.

In ML or Haskell, you'd introduce an algebraic data type R = cons1 of S | cons2 of T where R, S, and T are types and cons1 are constructors. In your terminology you'd call an alternative such as 'cons1 of S' a 'type' (a run-time type); the ML and Haskell communities call these things variants [of a type]. 

In dependently typed languages, say Agda or Cayenne, you can even specify that when f is given 1 it returns the left variant and when it is given 2 it returns the right one. (I am too uninformed to say whether you can literally return distinct types instead of distinct variants but I believe this to be the case.) 

In Typed Racket, you return a union type and you can then use subtyping to get the correct type back. 

So there's nothing wrong with such functions at all. There are only poor type systems and rich ones. 

-- Matthias