Changes between Version 2 and Version 3 of TypeLevelNamingIssues


Ignore:
Timestamp:
Oct 12, 2013 3:06:12 AM (22 months ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • TypeLevelNamingIssues

    v2 v3  
    1212sym :: (a :~: b) -> (b :~: a)
    1313trans :: (a :~: b) -> (b :~: c) -> (a :~: c)
    14 subst :: (a :~: b) -> a -> b
     14castWith :: (a :~: b) -> a -> b
    1515liftEq :: (a :~: b) -> (f a :~: f b)
    1616liftEq2 :: (a :~: a') -> (b :~: b') -> (f a b :~: f a' b')
     
    3131  Coercion :: Coercible a b => Coercion a b
    3232
    33 newtype Sym a b = Sym { unsym :: Coercion b a }
    3433coerceWith :: Coercion a b -> a -> b
    3534sym :: forall a b. Coercion a b -> Coercion b a
     
    107106These are in no particular order, but they are numbered for easy reference.
    108107
    109 1. What is the `Sym` newtype in `Data.Type.Coercion` all about?
     1081. `EqualityT` and `CoercionT` sound like monad transformers. I (Richard) have actually been confused by this at one point.
    110109
    111 2. `EqualityT` and `CoercionT` sound like monad transformers. I (Richard) have actually been confused by this at one point.
     1102. Should `KProxy`'s data constructor be named `KProxy`? Reusing the name here requires users to use a `'` every time they want to use the promoted data constructor `KProxy`.
    112111
    113 3. Should `KProxy`'s data constructor be named `KProxy`? Reusing the name here requires users to use a `'` every time they want to use the promoted data constructor `KProxy`.
     1123. There are up to three different ways type-level predicates can be defined: as Constraints, as GADTs wrapping constraints, or as type families returning `Bool`s. Is there a common naming convention among these? Right now, we have `(~)` (constraint) vs `(:~:)` (GADT); `(<=?)` (Boolean-valued) vs. `(<=)` (constraint); and `Coercible` (constraint) vs. `Coercion` (GADT).
    114113
    115 4. Are `SomeNat` and `SomeSymbol` necessary in !TypeLits? Do we expect these to be used widely?
     1144. `eqT` (from `Data.Typeable`) and `equalsT` (from `Data.Type.Equality`) have similar names, achieve similar functions, but are subtly different. This may or may not be confusing.
    116115
    117 5. There are up to three different ways type-level predicates can be defined: as Constraints, as GADTs wrapping constraints, or as type families returning `Bool`s. Is there a common naming convention among these? Right now, we have `(~)` (constraint) vs `(:~:)` (GADT); `(<=?)` (Boolean-valued) vs. `(<=)` (constraint); and `Coercible` (constraint) vs. `Coercion` (GADT).
    118 
    119 6. `eqT` (from `Data.Typeable`) and `equalsT` (from `Data.Type.Equality`) have similar names, achieve similar functions, but are subtly different. This may or may not be confusing.
    120 
    121 7. The name of the function currently called `subst` (from `Data.Type.Equality`) is up in the air. I (Richard) personally favor `castWith`.
    122 
    123 8. I (Richard) want to add the following function to `Data.Type.Equality`:
     1165. I (Richard) want to add the following function to `Data.Type.Equality`:
    124117{{{
    125118gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
     
    129122    I've tested this function in a real setting, and it (that is, type inference for it) works great.
    130123
    131 9. I propose the following, further addition to `Data.Type.Equality`:
     1246. I propose the following, further addition to `Data.Type.Equality`:
    132125{{{
    133126type family a == b where