edit: I have followed up with a more specific question. Thank you answerers here, and I think the followup question does a better job of explaining some confusion I introduced here.
TL;DR I'm struggling to get proofs of constraints into expressions, while using GADTs with existential constraints on the constructors. (that's a serious mouthful, sorry!)
I've distilled a problem down to the following. I have a simple GADT that represents points called X and function applications called F. The points X are constrained to be Objects.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
Constrained refers to containers whose objects are constrained by something and Object is that something. (edit: my real problem involves Category and Cartesian classes from constrained-categories)
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for ex
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
I would like to write an expression:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex0 :: GADT ix String
ex0 = F show (X (3 :: Int))
And while the obvious solution works, it quickly becomes verbose when building larger expressions:
-- Typechecks, but eventually verbose
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
I think the correct solution should look something like this:
-- error: Could not deduce: Object ix Int arising from a use of ‘X’
ex2 :: Constrained ix => GADT ix String
ex2 = F show (X (3 :: Int))
But I still can't get that proof of Object ix Int.
I'm sure it's simpler than I'm thinking. I have tried adding constraints to the Object constraint family in the GADT class instance. I have tried offering constraints in the expression's signature. I have tried QuantifiedConstraints, although, I'm not sure I fully grasp it yet. Please help me wise ones!
Runnable:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE InstanceSigs #-}
module Test where
import Data.Kind
import Data.Functor.Identity
import Data.Functor.Const
-- | I can constrain the values within containers of kind `* -> *`
class Constrained (ix :: * -> *) where
type Object ix a :: Constraint
-- | Here's a trivial constraint. A more interesting one might include `Typeable a`, for instance
instance Constrained (GADT ix) where
type Object (GADT ix) a = (Constrained ix, Object ix a)
-- | A demo GADT that has function application ('F'), and points ('X'). The
-- points are constrained.
data GADT ix a where
X :: Object ix a => a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
-- -- Broken
-- -- error: Could not deduce: Object ix Int arising from a use of ‘X’
-- ex0 :: GADT ix String
-- ex0 = F show (X (3 :: Int))
-- Typechecks
-- but for larger programs becomes verbose, requiring many explicit constraints
ex1 :: Object ix Int => GADT ix String
ex1 = F show (X (3 :: Int))
-- -- What I want, but, it's broken
-- ex2 :: Constrained ix => GADT ix String
-- ex2 = F show (X (3 :: Int))
CodePudding user response：
Without more context it's hard to say what's the best solution, but here are a couple of possibilities:
Avoid constraining at all
As it stands, your GADT doesn't seem to have much reason for restricting X to Object. Maybe this is just not needed?
data GADT ix a where
X :: a -> GADT ix a
F :: (a -> b) -> GADT ix a -> GADT ix b
Instead, the constraint could come from the outside when it's needed.
Bite the bullet of constraint lists, but make them nicer
If you have many different types in your expression that all need to fulfill the same constraint, you can use a helper like All
ex2' :: All (Object ix) '[Int] => GADT ix String
ex2' = F show (X (3 :: Int))
where there can be more types in the list in addition to Int; and/or you can make synonym constraints such as
type StdObjs ix = (Object ix Int, Object x Bool, ...)
ex2'' :: StdObjs ix => GADT ix String
ex2'' = F show (X (3 :: Int))
Propagate the constraints backwards through the data structure itself
If you do need the constraint on the X values, it may nevertheless be possible to express this in another way in the GADT. For example, if the function is not a general function but something that is already constrained to only accept Objects, you could have it like this:
data YourFunc ix a b where
YourFunc :: Object ix a => (a->b) -> YourFunc ix a b
show' :: Object ix Int => YourFunc ix Int String
show' = YourFunc show
This doesn't directly help with the problem you were asking about, but maybe the function is shared or something. You could even have something like
class Object ix a => InferrenceChain ix a where
type PreElem ix a :: Type
propInferrence :: (InferrenceChain ix (PreElem a) => r) -> r
and then
data YourFunc ix a b where
YourFunc :: InferrenceChain ix a
=> (PreElem a -> a) -> YourFunc (PreElem a) a
Then in the end you could proof the X constraint from just putting in Object ix String on the outside and recursing over propInferrence. But this would probably get quite fiddly.
CodePudding user response：
I think the correct solution should look something like this:
-- error: Could not deduce: Object ix Int >arising from a use of ‘X’ ex2 :: Constrained ix => GADT ix String ex2 = F show (X 3)
Unfortunately, this solution doesn't make any sense. The compiler is justified in pointing out that it doesn't know that Object ix Int is satisfied at this point, since all it knows is that Constrained ix may impose some constraint through Object ix Int.
A solution through quantification
So perhaps what you want is a constraint which says: "at this point, all Object ix a constraints I use are satisfied" - which we can try and do through quantification:
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
type Satisfied ix = forall a. Object ix a
ex2 :: Satisfied ix => GADT ix String
ex2 = F show (X 3)
Unfortunately, that gives us a GHC error:
• Quantified predicate must have a class or type variable head:
forall a. Object ix a
• In the quantified constraint ‘forall a. Object ix a’
In the type synonym declaration for ‘Satisfied’
Since Object is a type family and not a class or type variable.
Re-architecture
But... why is Object a type family? In fact, why does Constrained exist at all as a lawless class with no methods? If we want to exert constraints on combinations of containers and types, Haskell already gives us the means to do that - just use instance constraints!
{-# LANGUAGE MultiParamTypeClasses #-}
class Object ix a
type Constrained ix = forall a. Object ix a
Because if we have
instance (...<some stuff>...) => Constrained Foo where
type Object ix a = (...<some def>...)
we could translate that to
instance (...<some stuff>..., ...<some def>...)
=> Object ix a
Which makes this example compile.
ex2 :: Constrained ix => GADT ix String
ex2 :: F show (X 3)