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 |