[GHC] #11439: Request for comments: Allow duplicate type signatures
#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
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I do think something like this would be useful. But recall that type signatures and function definitions need not be next to each other. And I'm very suspicious of a proposal that cares about top-to-bottom ordering of definitions (nowhere else in Haskell is that done). On the other hand, this is a good idea for a pragma. Perhaps {{{ foo :: a -> a foo x = x {-# TYPECHECK foo :: Bool -> Bool foo :: Int -> Int foo :: Maybe a -> Maybe a foo True :: Bool map id [] #-} }}} The idea here is that the `TYPECHECK` pragma allows to you list a bunch of expressions. GHC checks that the expressions are well-typed. If one isn't, an error is issued. You could imagine Haddock looking for examples where the expression is a type signature for a bare variable and then using the types as extra documentation for that variable. While we're at it, I'd also love {{{ {-# ILL_TYPED map True False - 'x' #-} }}} If an expression in `ILL_TYPED` is actually well-typed, an error is issued. This would be very useful in putting in unit tests for fancy type- level features. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): I like that, GHCi could display associated types: {{{#!hs
:type sum sum :: SBool single -> IsSingleton single -> Natural
:types sum sum :: SBool single -> IsSingleton single -> Natural
sum STrue :: Natural -> Natural sum SFalse :: [Natural] -> Natural }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): It would also help simplify the FTP types, as well as showing possibly enlightening groupings (`(a -> b) -> (F a -> F b)` versus `(a -> b) -> F a -> F b`): {{{#!hs
:types length length :: Foldable t => t a -> Int
length :: [a] -> Int length :: Set a -> Int length :: Map k v -> Int }}} {{{#!hs
:types fmap fmap :: Functor f => (a -> b) -> f a -> f b
fmap :: Functor f => (a -> b) -> (f a -> f b) fmap :: (a -> b) -> ([a] -> [b]) fmap :: (a -> b) -> (Either e a -> Either e b) fmap :: (b -> c) -> (a -> b) -> (a -> c) }}} {{{#!hs
:types sequence sequence :: (Traversable t, Monad m) => t (m a) -> m (t a)
sequence :: Monad m => [m a] -> m [a] sequence :: [IO a] -> IO [a] sequence :: [Maybe a] -> Maybe [a] sequence :: [r -> a] -> (r -> [a]) sequence :: [[a]] -> [[a]] }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by adamgundry): * cc: adamgundry (added) Comment: I'm not really convinced by the original ticket: couldn't you just as well do something like {{{#!hs sum :: SBool single -> IsSingleton single -> Natural sum STrue = sumTrue sum SFalse = sumFalse sumTrue :: Natural -> Natural sumTrue x = x sumFalse :: [Natural] -> Natural sumFalse [] = 0 sumFalse (x : xs) = x + sumFalse xs }}} without needing any additional syntax or rules for associating duplicate signatures with parts of definitions? On the other hand, being able to declare a bunch of specializations such that GHCi or Haddock can display them does seem rather useful, especially for the kind of very polymorphic code you get in `lens` or the post-FTP Prelude. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:1 goldfire]:
On the other hand, this is a good idea for a pragma. Perhaps
{{{ foo :: a -> a foo x = x
{-# TYPECHECK foo :: Bool -> Bool foo :: Int -> Int foo :: Maybe a -> Maybe a foo True :: Bool map id [] #-} }}}
My gut feeling is that it must take local assumptions into account, swapping equations may confuse more than it helps (resulting from shifting equations around): {{{#!hs {-# TYPECHECK sum :: SBool False -> [Natural] -> Natural #-} sum STrue x = x {-# TYPECHECK sum :: SBool True -> Natural -> Natural #-} sum SFalse [] = 0 sum SFalse (x : xs) = x + sum SFalse xs }}} One of my syntax suggestions was an attempt to capture the local assumptions (#11387?): {{{#!hs sum @False :: SBool False -> [Natural] -> Natural sum @False SFalse :: [Natural] -> Natural }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Similar for type families: {{{#!hs type family Sing (res :: k -> Type) | res -> k where -- Sing :: Nat -> Type Sing = SingNat -- Sing :: Nat -> Type Sing = SingBool }}} Annotations work fine here `Sing = (SingNat :: Nat -> Type)`, ... but its utility is clearer in this [https://gist.github.com/AndrasKovacs/c7d385aa117929503feb gist] where we could annotate `(@@)` instances in different ways without modifying the definitions: {{{#!hs data Con1 :: (a -> b) -> (a ~> b) data Con2 :: (a -> b -> c) -> (a ~> b ~> c) data Con3 :: (a -> b -> c -> d) -> (a ~> b ~> c ~> d) type family (@@) (f :: a ~> b) (x :: a) :: b -- (@@) :: (a ~> b) -> (a -> b) type instance Con1 c @@ a = c a -- (@@) :: (a ~> b ~> c) -> a -> (b ~> c) -- (@@) :: (a ~> (b ~> c)) -> (a -> (b ~> c)) -- (@@) :: (a ~> b ~> c) -> (a -> b ~> c) type instance Con2 c @@ a = Con1 (c a) -- (@@) :: (a ~> b ~> c ~> d) -> a -> (b ~> c ~> d) -- (@@) :: (a ~> (b ~> c ~> d)) -> (a -> (b ~> c ~> d)) -- (@@) :: (a ~> b ~> c ~> d) -> (a -> b ~> c ~> d) type instance Con3 c @@ a = Con2 (c a) }}} I think this will only become more useful as GHC's type system evolves -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Replying to [comment:4 adamgundry]:
I'm not really convinced by the original ticket: couldn't you just as well do something like
On the other hand, being able to declare a bunch of specializations such
Yes you can at the expense of introducing extraneous definitions, your solution works fine for the original example but I fear it does not scale. that GHCi or Haddock can display them does seem rather useful, especially for the kind of very polymorphic code you get in `lens` or the post-FTP Prelude. Yes, I also emphasise parentheses to shift students' thinking from: {{{#!hs map :: (a -> b) -> [a] -> [b] }}} to {{{#!hs map :: (a -> b) -> ([a] -> [b]) }}} You would never create a new function to accomplish this minor task but maybe this definition of `fmap` would prove useful to some: {{{#!hs class Functor f where {-# TYPECHECK fmap :: (a -> b) -> (f a -> f b) #-} fmap :: (a -> b) -> f a -> f b }}} Who knows. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by niteria): * cc: niteria (added) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#11439: Request for comments: Allow duplicate type signatures -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: feature request | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.10.3 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by Iceland_jack): Collect uses in [https://gist.github.com/Icelandjack/f5247a4d7d29e76a364f2073efe9928c gist]. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11439#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC