Changes between Version 2 and Version 3 of TypeLevelNamingIssues


Ignore:
Timestamp:
Oct 12, 2013 3:06:12 AM (6 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