Type supplement for constructor specific uses of sum types

[gabrielrf]

Benefits: Avoid error calls (runtime), exception control and Maybe types in partially defined (constructor specific) functions on sum types

Method: by refining function argument types with a list of constructors applyable and detecting the target constructor at the caller through pattern matching, flagging with compiler errors the unmatched cases.

As an example, with

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

* Actual system: undefined cases are discriminated with runtime errors or exception throwing or optional Maybe results.

   hd :: List a -> a
   hd (Cons x _) -> x
   hd Nil -> error "error: hd: empty list" -- (as in GHC Data.List head)

* Proposed system: supplement types with

a suffix @Constructor or @{Constructor1, Constructor2}

denoting the list of constructors to which the function can be applied.

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

   -- no definition for unappropriate constructors.

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

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

using it:

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

   accumulateHead f accum list = case list of

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

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

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

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

(from Jason Dagit contribution)

Syntax {Cons, Cons2} for more than one constructor

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

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

Discussion thread:

 http://thread.gmane.org/gmane.comp.lang.haskell.cafe/75586

[gabrielrf]

Benefits: Avoid error calls (runtime), exception control and Maybe types in partially defined (constructor specific) functions on sum types

Method: by refining function argument types with a list of constructors applyable and detecting the target constructor at the caller through pattern matching, flagging with compiler errors the unmatched cases.

As an example, with

Error: Failed to load processor haskell

No macro or processor named 'haskell' found

* Actual system: undefined cases are discriminated with runtime errors or exception throwing or optional Maybe results.

Error: Failed to load processor haskell

No macro or processor named 'haskell' found

* Proposed system: supplement types with

a suffix @Constructor or @{Constructor1, Constructor2}

denoting the list of constructors to which the function can be applied.

Error: Failed to load processor haskell

No macro or processor named 'haskell' found

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

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

using it:

Error: Failed to load processor haskell

No macro or processor named 'haskell' found

(from Jason Dagit contribution) Syntax as {Cons, Cons2} for more than one constructor

Error: Failed to load processor haskell

No macro or processor named 'haskell' found

Discussion thread:

 http://thread.gmane.org/gmane.comp.lang.haskell.cafe/75586

[gabrielrf]

Benefits: Avoid error calls (runtime), exception control and Maybe types in partially defined (constructor specific) functions on sum types

Method: by refining function argument types with a list of constructors applyable and detecting the target constructor at the caller through pattern matching, flagging with compiler errors the unmatched cases.

As an example, with

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

* Actual system: undefined cases are discriminated with runtime errors or exception throwing or optional Maybe results.

   hd :: List a -> a
   hd (Cons x _) -> x
   hd Nil -> error "error: hd: empty list" -- (as in GHC Data.List head)

* Proposed system: supplement types with

a suffix @Constructor or @{Constructor1, Constructor2}

denoting the list of constructors to which the function can be applied.

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

   -- no definition for unappropriate constructors.

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

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

using it:

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

   accumulateHead f accum list = case list of

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

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

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

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

(from Jason Dagit contribution) Syntax {Cons, Cons2} for more than one constructor

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

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

Discussion thread:

 http://thread.gmane.org/gmane.comp.lang.haskell.cafe/75586

[gabrielrf]

Related theoretical article:  http://winterkoninkje.livejournal.com/56979.html

[gabrielrf]

Further extension:

since we try to propagate case analysis we can express the type supplement as a set of disjoint patterns, as masks for the different branches

hd :: (List2 a) @ { Cons a _ | Cons2 a _ _ } -> a
hd (Cons x _) = x
hd (Cons2 x _ _) = x

as reflected by Wren NG Thornton in  http://article.gmane.org/gmane.comp.lang.haskell.cafe/75669

making possible nested patterns

headFromJust :: (Maybe a) @ {Just a:_} -> a

[gabrielrf]

Correction. No need for type info within the supplement.

hd :: (List2 a) @ { Cons _ _ | Cons2 _ _ _ } -> a
hd (Cons x _) = x
hd (Cons2 x _ _) = x

headFromJust :: (Maybe a) @ {Just (_:_)} -> a

[gabrielrf]

Sorry

headFromJust :: (Maybe (List a)) @ {Just (_:_)} -> a

[gabrielrf]

Replying to gabrielrf:

Related theoretical article:  http://winterkoninkje.livejournal.com/56979.html

The type supplement could be seen as a type narrowing mechanism to the "difference types" explained in the article.

[gabrielrf]

Possible extension with "Negative patterns" to avoid out-of-domain function parameters :

as introduced by Wren NG Northon in  http://article.gmane.org/gmane.comp.lang.haskell.cafe/75669

given

case x of

v @ patt1 -> f v -- v @ patt2 -> f v -- pattern of v == patt2 \\ patt1 v @ _ -> f v -- pattern of v == _ \\ patt2 \\ patt1

inverse :: (Fractional a) => a @ { _ \\ 0.0} -> a inverse v = 1 / v

The type supplement @{ _ \\ 0.0} would tell the compiler to check that

the caller's case analysis should have evaluated the case for 0.0 in a previous case branch before calling to inverse

[gabrielrf]

sorry for the layout.

Possible extension with "Negative patterns" to avoid out-of-domain function parameters :

as introduced by Wren NG Northon in  http://article.gmane.org/gmane.comp.lang.haskell.cafe/75669

given

    case x of
      v @ patt1 -> f v    --
      v @ patt2 -> f v    -- pattern of v == patt2 \\ patt1
      v @ _ -> f v        -- pattern of v == _ \\ patt2 \\ patt1


inverse :: (Fractional a) => a @ { _ \\ 0.0} -> a       
inverse v = 1 / v

The type supplement @{ _ \\ 0.0} would permit the compiler to check that the caller's case analysis should have evaluated the case for 0.0 in a previous case branch before calling to inverse

[gabrielrf]

Final considerations:

Narrowing types with value patterns makes programming cleaner and safer.

Avoids the treatment of out-of-domain values in partially defined functions (like constructor-specific functions on sum types) with the corresponding use of calls to error, exception throwing or Maybe results.

The value patterns can be gathered at the caller through case analysis and assigned to as-pattern variables or as refinements of the case variable, and checked at compile time when used as actual parameters.

[igloo]

I think a proposal for a type system extension like this would be better worked out on the wiki, and discussed by e-mail, rather than as a trac ticket (where it will drown in the noise).

[simonpj]

See also Neil Mitchell's thesis  http://community.haskell.org/~ndm/thesis/. In particular his Catch tool, which has an analysis reminiscent of the one you suggest.

Simon