[Haskell-cafe] Type system extension

[Thomas Davie]

On May 16, 2005, at 12:46 AM, Neil Mitchell wrote:

> Hi,
>
> Yes, sounds like a good idea. I'm not sure the right approach is to
> make the user give this information though - the code will very likely
> be something like
>
> doSomethingToAModule (SModule a b) = f a b
>
> from which you can derive the type SCode(SModule) very easily. As the
> expressions get more complex, you will want more substantial
> annotations - i.e. SCode(SModule(_,[])|SUnknown) for something which
> either exports nothing, or is unknown. At this point getting the
> programmer to type in essentially the same information twice is likely
> to become annoying.
I'm not certain I agree with you.  Where I do agree is that the types  
are liable to get very complex fairly quickly, and this may well be  
the flaw in the plan, however, I think Haskell benefits greatly from  
asking the programmer to provide the same information twice in  
slightly different forms.

The type system after all is essentially a method of providing a  
sanity check -- "does the code actually match up with what the  
programmer specified as a type".

> My current work on my PhD is all related to checking that a Haskell
> program cannot raise a pattern match error, and it is accomplished in
> a similar sort of method to what you are suggesting, and achieves
> similar goals. This work is still ongoing, but a first order checker
> exists for a subset of Haskell already - so progress is being made.
I haven't thought about this for more than half a day when the idea  
popped into my head, so obviously you've dealt with it a bit more,  
but I wonder if this is only half the problem.  By the sounds of it  
you are doing type inferencing from the program (as you explained  
above), which allows for a certain level of checks.  However, type  
errors are not only thrown when the type inference system can't  
generate types to fit the program, but also when the programmer has  
specified types that are different to that the inference worked out.

Thanks for a very interesting reply

Tom Davie