[Haskell-cafe] Re: Proposal: Sum type branches as extended types (as Type!Constructor)

[Gabriel Riba]

Edward Kmett suggests the use of @ instead of !

Edward Kmett wrote:

This is just a form of refinement type. Googling the term should turn up a
 couple dozen papers on the topic.

You can emulate them (and more) with phantom types in the existing 
 type system, though admittedly the encoding is occasionally uncomfortable. 
  As a result there hasn't been much interest in them from on high.

And a minor technical issue with the use of ! there is that it would be 
  awkward from a grammar perspective because it would require that ! bind 
  more tightly than juxtaposition, but only when parsing a type. 
  Another syntactic operator like @ that already binds very tightly 
  might be more appropriate.

-Edward Kmett

New proposal draft:

Proposal: Type supplement for constructor specific uses of sum types

Purpose: Avoid error clauses (runtime errors), exception control or Maybe
 types in partially defined (constructor specific) functions on sum types.

As an example, with

   data List a = Nil | Cons a (List a)  

* Actual system, with runtime errors (as in GHC Data.List head) or 
exception throwing or optional Maybe results.

   hd :: List a -> a
   hd (Cons x _) -> x
   hd Nil -> error "error: hd: empty list" -- error or exception throwing

* Proposed system extending types with a suffix @ Constructor or @
{Constructor1, Constructor2, ..}

   hd :: List @ Cons a -> a
   hd (Cons x _) = x

The caller must do pattern matching before applying the constructor-specific
function.

In ''var @ (Constructor {})'' the compiler should set a type supplement
property for ''var'' to the specified pattern constructor and check 
the supplement when used in a constructor specific parameter position.


using it:

   accumHead :: (a->b) -> a -> List a -> b

   accumHead f accum list = case list of

        li @ Cons {} -> f accum $ hd li  -- typeSupplementOf li == 'Cons'
                                  -- should pass typechecker at ''hd'' for List!Cons

        li @ Nil  -> f accum $ hd li     -- compiler error !! 
                                -- typeSupplementOf li == 'Nil' ; no match

        _ -> f accum $ hd list           -- compiler error !! 
                               -- typeSupplementOf list == Nothing ; no match

        _ -> accum       -- default closing pattern matching exhaustivity.

(from Jason Dagit contribution) For more than one constructor say 

  data List2 a = Nil | Cons a (List2 a) | Cons2 a a (List2 a)

hd :: List2 @ {Cons, Cons2} a -> a