I was reading:
Summer School on Generic and Effectful Programming Applying Type-Level and Generic Programming in Haskell Andres Löh, Well-Typed LLP https://www.cs.ox.ac.uk/projects/utgp/school/andres.pdf and trying out the various code fragments, and was mildly surprised by the need for -XUndecidableInstances when deriving the 'Show' instance for the heterogenous N-ary product 'NP': deriving instance All (Compose Show f) xs => Show (NP f xs) Without "UndecidableInstances" I get: • Variable ‘k’ occurs more often in the constraint ‘All (Compose Show f) xs’ than in the instance head ‘Show (NP f xs)’ (Use UndecidableInstances to permit this) • In the stand-alone deriving instance for ‘All (Compose Show f) xs => Show (NP f xs)’ This is not related to automatic deriving, as a hand-crafted instance triggers the same error: instance All (Compose Show f) xs => Show (NP f xs) where show Nil = "Nil" show (x :* xs) = show x ++ " :* " ++ show xs Is there some other way of putting together the building blocks that avoids the need for 'UndecidableInstances', or is that somehow intrinsic to the type of NP construction? I guess I should also ask whether there's a way to define something equivalent to 'Compose' without 'UndecidableSuperClasses', and perhaps the two are not unrelated. [ Perhaps I should be more blasé about enabling these extensions, but I prefer to leave sanity checks enabled when possible. ] -- Viktor. {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} import GHC.Exts (Constraint) -- | Map a constraint over a list of types. type family All (c :: k -> Constraint) (xs :: [k]) :: Constraint where All _ '[] = () All c (x ': xs) = (c x, All c xs) -- | With @g@ a type constructor and @f@ a constraint, define @Compose f g@ as -- a contraint on @x@ to mean that @g x@ satisfies @f@. -- -- Requires: -- -- 'ConstraintKinds' -- 'FlexibleInstances' -- 'MultiParamTypeClasses' -- 'TypeOperators' -- 'UndecidableSuperClasses' -- class (f (g x)) => (Compose f g) x instance (f (g x)) => (Compose f g) x -- | Type-level 'const'. newtype K a b = K { unK :: a } deriving instance Show a => Show (K a b) -- | N-ary product over an index list of types @xs@ via an interpretation -- function @f@, constructed as a list of elements @f x@. -- data NP (f :: k -> *) (xs :: [k]) where Nil :: NP f '[] (:*) :: f x -> NP f xs -> NP f (x ': xs) infixr 5 :* -- | If we can 'show' each @f x@, then we can 'show' @NP f xs@. -- -- Requires: 'UndecidableInstances' -- deriving instance All (Compose Show f) xs => Show (NP f xs) _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
On Sun, Dec 01, 2019 at 03:36:58PM +1300, Anthony Clayden wrote:
> > ... was mildly surprised by the need for -XUndecidableInstances when > > deriving the 'Show' instance for the heterogenous N-ary product > > 'NP': > > There's been much debate: should we find a less scary name? Perhaps, though the old name would have to stick around as an alias for a few major releases. But if the idea is to discourage the use of the extension when not essential, it's working! :-) > Presumably your program compiles and runs OK with that switched on(?) Yes. > > I guess I should also ask whether there's a way to define something > > equivalent to 'Compose' without 'UndecidableSuperClasses', and > > perhaps the two are not unrelated. > > Not exactly related, but again superclass instance resolution wants to > make the problem smaller at each step. The definition for class > Compose has a constraint no smaller than the class head (3 variables). What surprises me about 'Compose' is that it is not really trying to define a class as such, rather it aims to construct a new constraint (family) from an existing one. The definition feels like a subtle hack, used only for lack of a more natural syntax: http://hackage.haskell.org/package/type-combinators-0.2.4.3/docs/src/Type-Family-Constraint.html#Comp class d (c a) => Comp (d :: l -> Constraint) (c :: k -> l) (a :: k) instance d (c a) => Comp d c a I'd have expected instead something more akin to: type family Comp2 (c :: l -> Constraint) (f :: k -> l) :: k -> Constraint where Comp2 c f = \x -> c (f x) -- Oops, no type-level lambdas -- or Comp2 c f x = c (f x) -- Oops, too many LHS parameters but there seems to be no direct way to express this type of composite constraint, without inventing the clever paired class and instance. While I can write: type family Comp2 (c :: l -> Constraint) (f :: k -> l) (x :: k) :: Constraint where Comp2 c f x = c (f x) And partial application of Comp2 even has the expected kind: λ> :k Comp2 Show (K Int) Comp2 Show (K Int) :: k -> Constraint sadly, one can't actually use "Comp2 Show f": λ> deriving instance All (Comp2 Show f) xs => Show (NP f xs) • The type family ‘Comp2’ should have 3 arguments, but has been given 2 • In the context: All (Comp2 Show f) xs While checking an instance declaration In the stand-alone deriving instance for ‘All (Comp2 Show f) xs => Show (NP f xs)’ So the class/instance pair seems to be the only way. > Yes that's a sensible policy. The trouble with -XUndecidableInstances > is that it's a module-wide setting, so lifts the check for all > instances of all classes. So it seems best to isolate the code that needs this in as a small module as possible, and do without everywhere else. -- Viktor. _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post. |
Free forum by Nabble | Edit this page |