#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