[Haskell-cafe] Re: [Haskell] View patterns in GHC: Requestforfeedback

[Claus Reinke]

> Oh!  I had assumed that it was already considered rude to expose a
> non-exhaustive function to the outside world: 

you mean, as in: head, tail, fromJust, ..?-)

whether exposing or using those is considered rude or not, the type 
system has nothing to tell us about their not handling some inputs, 
and if you get them from precompiled libraries, you don't see the 
compiler warnings, either.

>> one could turn that promise into a type-checked guarantee by using
>> explicit sum types (and thus structural rather than name-based typing),
>> but that gets awkward in plain haskell.
> 
> I don't think the choice of whether you label your variants with names
> or with numbers (in1, in2, in3...) has anything to do with the choice of
> whether you require your cases to be exhaustive or not.

i was talking about name-based (as in: this is the sum type named List) 
vs structural (as in: this is the sum type build from Cons and Nil) typing.
the former hides (in-)exhaustiveness from the type system, the latter
exposes it. 

consider the example code below, where the type system catches the 
non-exhaustiveness of g, where the sum structure of its parameter is 
exposed, but has nothing to say about f, where the sum structure is 
hidden behind a type name.
 
claus

{-# OPTIONS_GHC -fallow-overlapping-instances #-}
{-# OPTIONS_GHC -fglasgow-exts #-}

{- our own, nameless sum type with injection and unpacking -}
infixr :|
data a :| b 
data a :< b = Inj a deriving Show

class    Inj a b                 where { inj   :: a -> a:<b ; out         :: a:<b -> a }
instance Inj a a                 where { inj a  = Inj a     ; out (Inj a)  = a }
instance Inj a (a:|b)            where { inj a  = Inj a     ; out (Inj a)  = a }
instance Inj a b => Inj a (c:|b) where { inj a  = Inj a     ; out (Inj a)  = a }

{- a product type of nested pairs, with selection -}
class    Sel a b                where sel       :: b -> a
instance Sel a a                where sel a      = a
instance Sel a (a,b)            where sel (a,_)  = a
instance Sel a b => Sel a (c,b) where sel (_,b)  = sel b

{- to match, supply a product of functions covering the sum -}
match :: (Inj x xs, Sel (x->b) fs) => x:<xs -> fs -> b
match x fs = sel fs (out x)

{- example A: nameless sum -}
type Sum = String :| Char :| Bool

g y = match y (\s->s::String,
              (\c->c:""
              ))
              -- ,(\b->if b then "1" else "2")))

{- example B: named sum -}
data NamedSum = S String | C Char | B Bool deriving Show

f :: NamedSum -> String
f (S s) = s
f (C c) = c:""
-- f (B b) = if b then "1" else "2"

{- testing -}
main = do
  putStrLn $ g (inj "hi"  :: String:<Sum)
  putStrLn $ f (S "ho"    :: NamedSum)
  putStrLn $ g (inj 'x'   :: Char:<Sum)
  putStrLn $ f (C 'y'     :: NamedSum)
  putStrLn $ g (inj False :: Bool:<Sum)
  putStrLn $ f (B True    :: NamedSum)