[GHC] #11439: Request for comments: Allow duplicate type signatures

[GHC]

#11439: Request for comments: Allow duplicate type signatures
-------------------------------------+-------------------------------------
           Reporter:  Iceland_jack   |             Owner:
               Type:  feature        |            Status:  new
  request                            |
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  7.10.3
           Keywords:                 |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Interested in feedback (Code inspired by
 [http://www.cs.ox.ac.uk/projects/utgp/school/idris-tutorial.pdf Idris
 tutorial])

 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural
 sum STrue  x        = x
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}


 Allow duplicate type signatures:
 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural

 sum :: SBool True -> Natural -> Natural
 sum STrue  x        = x

 sum :: SBool False -> [Natural] -> Natural
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}


 Where

 {{{#!hs
 data SBool b where
   STrue  :: SBool True
   SFalse :: SBool False

 type family
   IsSingleton (b :: Bool) :: Type where
   IsSingleton True  = Natural
   IsSingleton False = [Natural]
 }}}

 ----

 == Behaviour ==
 You could do something fancy but I would be happy with a check that any
 duplicate type signature is a specialization of the ''top'' top-level one,
 this would allow something like this:

 {{{#!hs
 length :: [a]  -> Int
 length :: [()] -> Int
 length []     = 0
 length (_:xs) = 1 + length xs
 }}}

 Which isn't very useful, hah what ever.

 ----

 == Benefits ==
 Mainly compiler-checked documentation, for the `sum` function we make it
 clearer that a `STrue` gives you `Natural -> Natural` while `SFalse` gives
 you `[Natural] -> Natural`. This is most apparent in the final syntax
 idea:

 {{{#!hs
 sum    :: SBool single -> IsSingleton single -> Natural

 @True  :: _ -> Natural   -> Natural
 @False :: _ -> [Natural] -> Natural
 }}}

 Reader need not look at definition of `IsSingleton`, it is fully described
 by the duplicate signatures.

 See ''lens'' where most functions have some kind of type specialisation
 declared in comments: [https://hackage.haskell.org/package/lens-4.13/docs
 /Control-Lens-Fold.html#v:-94--63- (^?)] whose type is `(^?) :: s ->
 Getting (First a) s a -> Maybe a`:

 {{{#!hs
 (^?) :: s -> Getter     s a -> Maybe a
 (^?) :: s -> Fold       s a -> Maybe a
 (^?) :: s -> Lens'      s a -> Maybe a
 (^?) :: s -> Iso'       s a -> Maybe a
 (^?) :: s -> Traversal' s a -> Maybe a
 }}}

 ----

 == Alternative syntax ==
 Throwing it out there, regardless of ambiguity:

 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural

     :: SBool True  -> Natural -> Natural
 sum STrue  x        = x

     :: SBool False -> [Natural] -> Natural
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}
 or
 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural

 ... :: SBool True -> Natural -> Natural
 sum STrue  x        = x

 ... :: SBool False -> [Natural] -> Natural
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}
 or
 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural

 ... @True  :: _ -> Natural -> Natural
 sum STrue  x        = x

 ... @False :: _ -> [Natural] -> Natural
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}
 or
 {{{#!hs
 sum :: SBool single -> IsSingleton single -> Natural

 @True  :: _ -> Natural -> Natural
 sum STrue  x        = x

 @False :: _ -> [Natural] -> Natural
 sum SFalse []       = 0
 sum SFalse (x : xs) = x + sum SFalse xs
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/11439>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler