Changes between Initial Version and Version 1 of SafeRoles/RolesOverview

Apr 30, 2015 1:04:43 AM (5 years ago)



  • SafeRoles/RolesOverview

    v1 v1  
     1= Roles Overview =
     3GHC 7.10 and later include a new implementation of GND that fixes the type-safety issues of previous versions.
     5However, it also introduces a new concept of representation equality, that is, two types that have the same in-memory representation. This is to allow 'safe' casting from one type to another when they have representational equality, allowing newtypes to finally have no performance overhead.
     7For example, before representational equality was introduced, the following code exacted a performance penalty:
     10newtype N = MkN { unN :: Int }
     12nsToInts :: [N] = [Int]
     13nsToInts = map unN
     16Even though it's equivalent to `id`, GHC keeps a typed intermediate representation and can't optimize across the type conversion.
     18=== Data.Coerce ===
     20The `Data.Coerce` package defines a new type-class:
     23class Coercible a b
     25coerce :: Coercible * a b => a -> b
     28The `Coercible` type-class can't be instantiated by hand, instead GHC will infer and generate them for two types with the same run-time representation.
     30GHC generate three kinds of instances. First, the trivial base case:
     33instance a a
     36Secondly, two instance exist for every `newtype NT = MkNT T`:
     39instance Coercible a T => Coercible a NT
     40instance Coercible T b => Coercible NT b
     43These two instances are only available if the `MkNT` constructor is in scope. They are called '''unwrapping instances'''.
     45Thirdly, for every type constructor (including newtype) there is an instance that allows coercion under the type. For example, let D be a type constructor (`data` or `newtype`) with three type arguments, which have roles nominal, representational, and phantom respectively. Then there is an instance of the form:
     48instance Coercible b b' => Coercible (D a b c) (D a b' c')
     51These instances are called '''lifting instances'''.
     53This means that by default, as a library author of a type constructor like `Set a`, users of your library will have access to `coerce :: Set T -> Set NT`.
     55To prevent this, you need to set the role of Set's type parameter to nominal by writing:
     58type role Set nominal
     61=== Roles ===
     63The goal of the roles system is to track when two types have the same
     64underlying representation. For example:
     67newtype Age = MkAge Int
     69type family Inspect x
     70type instance Inspect Age = Int
     71type instance Inspect Int = Bool
     73class BadIdea a where { bad :: a -> Inspect a }
     74instance BadIdea Int where { bad = (> 0) }
     75deriving instance BadIdea Age -- not allowed!
     78If the derived instance was allowed, the type would be `bad :: Age -> Instpect Age`, which is equivalent to `bad :: Age -> Int`, and so if we simply used the `BadIdea Int` dictionary, then we'd produce a `Bool` when an `Int` is expected. Roles track how type variables are used to make sure
     79such things can't happen!
     81A role declares how a type parameter affects the equality of a type constructor when we have two applications that differ only in one parameter. For example:
     84x :: T Age Bool c
     85y :: T Int Bool c
     88Do `x` and `y` have representational equality? The role for the first type parameter of `T` determines this.
     90There are three roles: representational, nominal and phantom.
     92==== Representational ====
     95data Simple a = MkSimple a -- a has role representational
     98The most common, and default, case is representational. This role allows
     99coercion between the outer type when we the inner types are equal. For example:
     102newtype MyInt = MkMyInt Int
     104toMyInt :: Simple Int -> Simple MkMyInt
     105toMyInt = coerce
     108==== Nominal ====
     111type family F
     112type instance F Int = Bool
     113type instance F Age = Char
     115data Complex a = MkComplex (F a) -- a has role nominal
     118Inferred when a type parameter may no longer have equivalent run-time
     119representation despite the arguments having equality.
     121==== Phantom ====
     124data Phant a = MkPhant Bool -- a has role phantom
     127Inferred when the type parameter doesn't affect the run-time representation of
     128the outer type.
     130==== Role Annotations (-XRoleAnnotations) ====
     133type role T nominal _ representational
     134data T a b c = MkT a b
     137Roles have an ordering, `nominal > representational > phantom`, and annotations
     138can only declare a type parameter to be a higher or equal role to the one
     141== Roles & Safe Haskell ==
     143Roles are an unfortunate mechanism for control right now. Since
     144representational is the default role for most type constructors, to enforce
     145invariants on abstract data types, library authors need to set their type
     146constructors to have nominal roles.
     148This requires that library authors understand roles to enforce what they expect
     149to happen according to Haskell2010 semantics. It also prevents them using
     150`coerce` internally and gaining the optimization, which is insulting as they
     151can write the code that coerce is semantically equivalent to.
     153It seems a different approach is needed, of either:
     1551) Require that all constructors are in scope when calling `coerce`. There is
     156some precedence for this as 7.10 requires that a newtype's constructor is in
     157scope to use `coerce`.
     159**NO**: This was requirement wasn't place of data types since some types (like
     160`IORef`) don't even have constructors that can be in scope.
     1622) Allow specifying internal + external role annotations.
     1643) Change the default to be nominal when all the constructors aren't exported,
     165and allow weakening of this to referential with role annotations.