We have a constraint (a~b) that can appear in a type signature
f :: (a~b) => a -> b
We can also have a type-level equality function
type family Eq a b where
Eq a a = True
Eq a b = False
The type-level Boolean reflects the (a~b) constraint precisely.
You sound as if you want a type family Satisfied, so you
type family Satisfied :: Constraint -> Bool
Then you could have
instance Ord T where ...
type instance Satisfied (Ord T) = True
The difficulty is that we can never return False, because you can always make T
an instance of Ord "later". And you can't have Satisfied (Ord T) returning
True in one place and Falsie in another. It can get stuck (not reduce) but it
can't return False.
I don't know if this would be useful to you.
And for more complex instances lie
instance Ord a => Ord [a]
I don't know what you want to say for
type instance Satisfied (Ord a) = ???
Simon
From: Libraries [mailto:[email protected]] On Behalf Of Ryan Newton
Sent: 15 October 2013 04:03
To: Pedro Magalhães ([email protected])
Cc: Haskell Libraries; Andres Löh; Ganesh Sittampalam; [email protected]
Subject: Re: Proposal: GHC.Generics marked UNSAFE for SafeHaskell
Hey, that's an awesome formulation! Thanks Pedro.
Any idea how much work this would be to implement in GHC, if it did garner
approval?
On Tue, Oct 8, 2013 at 3:48 AM, José Pedro Magalhães
<[email protected]<mailto:[email protected]>> wrote:
Hi,
On Mon, Oct 7, 2013 at 10:32 AM, Dag Odenhall
<[email protected]<mailto:[email protected]>> wrote:
Here's a thought: doesn't Generic already have an unused phantom type that's
only there "just in case we need to add something in the future"?
No, it doesn't.
Just a thought: what if we had a type family
type family Derives (t :: k1) (c :: k2) :: Bool
which would automatically be instantiated by GHC appropriately? E.g., if the
user had the following code:
data MyData = MyData deriving (Eq, Generic)
deriving instance Show MyData
instance Ord MyData
GHC would automatically instantiate:
type instance Derives MyData Eq = True
type instance Derives MyData Generic = True
type instance Derives MyData Show = True
type instance Derives MyData Ord = False
Would this be something Ryan could use for detecting safe instances for LVish?
Cheers,
Pedro
_______________________________________________
ghc-devs mailing list
[email protected]<mailto:[email protected]>
http://www.haskell.org/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/ghc-devs
