Changes between Version 2 and Version 3 of TypeLevelNamingIssues
 Timestamp:
 Oct 12, 2013 3:06:12 AM (4 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

TypeLevelNamingIssues
v2 v3 12 12 sym :: (a :~: b) > (b :~: a) 13 13 trans :: (a :~: b) > (b :~: c) > (a :~: c) 14 subst:: (a :~: b) > a > b14 castWith :: (a :~: b) > a > b 15 15 liftEq :: (a :~: b) > (f a :~: f b) 16 16 liftEq2 :: (a :~: a') > (b :~: b') > (f a b :~: f a' b') … … 31 31 Coercion :: Coercible a b => Coercion a b 32 32 33 newtype Sym a b = Sym { unsym :: Coercion b a }34 33 coerceWith :: Coercion a b > a > b 35 34 sym :: forall a b. Coercion a b > Coercion b a … … 107 106 These are in no particular order, but they are numbered for easy reference. 108 107 109 1. What is the `Sym` newtype in `Data.Type.Coercion` all about?108 1. `EqualityT` and `CoercionT` sound like monad transformers. I (Richard) have actually been confused by this at one point. 110 109 111 2. `EqualityT` and `CoercionT` sound like monad transformers. I (Richard) have actually been confused by this at one point.110 2. 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`. 112 111 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`.112 3. There are up to three different ways typelevel 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); `(<=?)` (Booleanvalued) vs. `(<=)` (constraint); and `Coercible` (constraint) vs. `Coercion` (GADT). 114 113 115 4. Are `SomeNat` and `SomeSymbol` necessary in !TypeLits? Do we expect these to be used widely?114 4. `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. 116 115 117 5. There are up to three different ways typelevel 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); `(<=?)` (Booleanvalued) 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`: 116 5. I (Richard) want to add the following function to `Data.Type.Equality`: 124 117 {{{ 125 118 gcastWith :: (a :~: b) > ((a ~ b) => r) > r … … 129 122 I've tested this function in a real setting, and it (that is, type inference for it) works great. 130 123 131 9. I propose the following, further addition to `Data.Type.Equality`:124 6. I propose the following, further addition to `Data.Type.Equality`: 132 125 {{{ 133 126 type family a == b where