[Haskell-cafe] Type system extension

[Neil Mitchell]

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.

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.

Thanks

Neil
www.cs.york.ac.uk/~ndm/

On 5/15/05, Thomas Davie <tom.davie at gmail.com> wrote:
> Hi,
>    I'd just been writing some code and an interesting idea for an
> extension to Haskell's type system sprang into my head.  I have no
> idea if people have played with it, but it looked vaguely useful to
> me, so I thought I'd see what everyone else thought.
> 
> Supposing you have these types:
> 
> type Export = String
> 
> data SCode = SModule String [Export] | SUnknown
> 
> It would be useful to specify a function as so:
> doSomethingToAModule :: SCode(SModule) -> SomeRandomOtherType
> 
> which would specify, not only that the first argument was of type
> SCode, but more specifically, that it used the SModule constructor.
> This would then allow you to safely only write a case for the SModule
> constructor, and not worry about a runtime error when pattern
> matching failed on an SUnknown (as this would be checked at compile
> time).
> 
> I hope this makes sense
> 
> What does anyone think of the idea, and is there an obvious flaw in
> the plan?
> 
> Thanks
> 
> Tom Davie
> 
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>