[Haskell-cafe] Type system extension

[Claus Reinke]

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).