Created
October 14, 2012 01:05
-
-
Save nfrisby/3886828 to your computer and use it in GitHub Desktop.
uninstantiable family for safe polykinded universally quantified constraints?
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE TypeFamilies, PolyKinds, ConstraintKinds, Rank2Types, | |
ScopedTypeVariables #-} | |
{-# LANGUAGE FlexibleInstances, UndecidableInstances, MultiParamTypeClasses | |
#-} -- only for examples | |
module Proposed.Data.Constraint.Forall | |
(module Data.Constraint, | |
Forall, Bottom, inst) where | |
import Unsafe.Coerce (unsafeCoerce) | |
import Data.Constraint (Dict(..), Constraint) | |
-- | Seriously, do not instantiate this type family; it is a source of | |
-- polykinded skolem variables, and soundness is compromised if it is | |
-- instantiated. | |
type family DO_NOT_INSTANTIATE (x :: k -> Constraint) :: k | |
-- safe to export, since | |
-- | |
-- 1) it can't be used to instantiate the family | |
-- 2) it can't be used to decompose the skolems (family not injective) | |
-- | |
-- ... right? | |
type Bottom x = DO_NOT_INSTANTIATE x | |
-- safe because @Bottom p@ is irreducible and not a value (ie not a type | |
-- constructor); ie it's a skolem type term. Thus @Forall p@ is satisfied iff | |
-- @p@ is parametric wrt its next parameter. | |
-- | |
-- Only nestings of @Forall@ could possibly result in the unsound reuse of the | |
-- same skolem type term for distinct quantified variables, but that nesting is | |
-- prevented by making @p@ a parameter to @Bottom@ -- explained below. | |
inst :: forall p t. Forall p => Dict (p t) | |
inst = unsafeCoerce (Dict :: Dict (p (Bottom p))) | |
-- WWe include the constraint itself in the skolem variable's syntactic | |
-- representation. This makes all skolem variables in scope distinct when | |
-- @Forall@s are nested. Such nesting is required in order for the use of | |
-- @unsafeCoerce@ in @inst@ to be unsound. But the construction of such | |
-- nestings requires intermediate class definitions (like @Forall2@ below) in | |
-- order to thread through the environment of other quantified | |
-- variables. Because those threading classes now end up as part of each skolem | |
-- type's syntactic representation, each variable in the environment is | |
-- syntactically distinct, and so soundness is maintained. | |
type Forall (p :: k -> Constraint) = p (Bottom p) | |
data Proxy (t :: k) = Proxy | |
class C (t :: k) where | |
method :: Proxy t -> String | |
instance C (t :: *) where | |
method _ = "*" | |
instance Functor t => C (t :: * -> *) where | |
method _ = "functor" | |
test_good = case inst :: Dict (C Int) of Dict -> method (Proxy :: Proxy Int) | |
-- ill-typed | |
-- test_bad = case inst :: Dict (C []) of Dict -> method (Proxy :: Proxy []) | |
class EQ (a :: *) (b :: *) where cast :: a -> b | |
instance EQ a a where cast = id | |
class Forall (c a) => Forall2 c a | |
instance Forall (c a) => Forall2 c a | |
-- ill-typed with this implementation; would be well-typed if @Bottom@ took no | |
-- argument | |
-- | |
--test_evil :: Int | |
--test_evil = case inst :: Dict (Forall2 EQ Char) of | |
-- Dict -> case inst :: Dict (EQ Char Int) of | |
-- Dict -> cast 'c' | |
-- | |
-- No instance for (EQ | |
-- (DO_NOT_INSTANTIATE (Forall2 EQ)) | |
-- (DO_NOT_INSTANTIATE | |
-- (EQ (DO_NOT_INSTANTIATE (Forall2 EQ))))) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
-- this files supplants these definitions from the constraints package: | |
-- | |
-- type ForallF (p :: * -> Constraint) (f :: * -> *) = (p (f A), p (f B)) | |
-- type ForallT (p :: * -> Constraint) (t :: (* -> *) -> * -> *) = (p (t F A), p (t M B)) | |
-- | |
-- as well as instF and instT | |
-- an auxiliary for ForallF | |
class p (f a) => CompositionInOne p f a | |
instance p (f a) => CompositionInOne p f a | |
type ForallF p f = Forall (CompositionInOne p f) | |
instF :: forall p f a. ForallF p f => Dict (p (f a)) | |
instF = case inst :: Dict (CompositionInOne p f a) of | |
Dict -> Dict | |
test_monoid :: forall f a. ForallF Monoid f => Dict (Monoid (f a)) | |
test_monoid = instF | |
-- using nesting for two quantifiers | |
class Forall (p a) => Forall_Once_Nested p a | |
instance Forall (p a) => Forall_Once_Nested p a | |
type Forall2 p = Forall (Forall_Once_Nested p) | |
inst2 :: forall p a b. Forall2 p => Dict (p a b) | |
inst2 = case inst :: Dict (Forall_Once_Nested p a) of | |
Dict -> case inst :: Dict (p a b) of | |
Dict -> Dict | |
-- an auxiliary for ForallT | |
class p (t a b) => CompositionInTwo p t a b | |
instance p (t a b) => CompositionInTwo p t a b | |
type ForallT p t = Forall2 (CompositionInTwo p t) | |
instT :: forall p t a b. ForallT p t => Dict (p (t a b)) | |
instT = case inst2 :: Dict (CompositionInTwo p t a b) of | |
Dict -> Dict |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment