Re: [Haskell-cafe] Type system extension
Hi Thomas,
this reminded me of GADTs
http://www.haskell.org/ghc/docs/6.4/html/users_guide/gadt.html
a first attempt is appended below, although you might find it
difficult to use in practice, because of the static guarantee.
cheers,
claus
--
{-# OPTIONS -fglasgow-exts #-}
type Export = String
data SModule
data SUnknown
data SCode a where
SModule :: String - [Export] - SCode SModule
SUnknown :: SCode SUnknown
doSomethingToAModule :: SCode SModule - String
doSomethingToAModule (SModule s es) = s
-- doSomethingToAModule SUnknown = oops
main = putStrLn $ doSomethingToAModule (SModule hi [])
-- main = putStrLn $ doSomethingToAModule SUnknown
-- type-checks and works as given in ghci-6.4.1
-- adding the second doSomethingToAModule line results in:
-- Scode.hs:14:21:
-- Inaccessible case alternative: Can't match types `SUnknown' and `SModule'
-- When checking the pattern: SUnknown
-- In the definition of `doSomethingToAModule':
-- doSomethingToAModule SUnknown = oops
-- Failed, modules loaded: none.
-- using the second main alternative results in:
-- Scode.hs:17:39:
-- Couldn't match `SModule' against `SUnknown'
-- Expected type: SCode SModule
-- Inferred type: SCode SUnknown
-- In the first argument of `doSomethingToAModule', namely `SUnknown'
-- In the second argument of `($)', namely `doSomethingToAModule SUnknown'
-- Failed, modules loaded: none.
--
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).
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system extension
Hello Thomas,
Sunday, May 15, 2005, 7:26:11 PM, you wrote:
TD data SCode = SModule String [Export] | SUnknown
TD It would be useful to specify a function as so:
TD doSomethingToAModule :: SCode(SModule) - SomeRandomOtherType
because constructor names are globally unique, this can be written just as:
doSomethingToAModule :: SModule - SomeRandomOtherType
i also needed similar feature, but to keep data as part of complex
structure:
data X = X { field1 :: SModule
, field2 :: ...
}
if Haskell will allow to define new types by or'ing existing ones,
whis will solve both our problems (modulo syntax sugar):
data SModule = SModule String [Export]
data SUnknown = SUnknown
data SCode= SModule | SUnknown
this extension will even allow to create ad-hoc polymorphic functions
(!). but on other side - increased complexity and ambiguousity of type
inferencing
may be, adding only ability to decompose existing multi-variant
types, but not to compose arbitrary types will not give such pressure
on type inferencing system
--
Best regards,
Bulatmailto:[EMAIL PROTECTED]
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Type system extension
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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system extension
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 [EMAIL PROTECTED] 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Type system extension
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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
