Request for comments: Allow duplicate type signatures

Interested in feedback (Code inspired by Idris tutorial)

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:

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

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:

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:

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: (^?) whose type is (^?) :: s -> Getting (First a) s a -> Maybe a:

(^?) :: 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:

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

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

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

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

Trac metadata

Trac field	Value
Version	7.10.3
Type	FeatureRequest
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture