Changes between Version 12 and Version 13 of Plugins/TypeChecker/RowTypes/Coxswain
 Timestamp:
 Sep 18, 2017 3:48:15 PM (2 years ago)
Legend:
 Unmodified
 Added
 Removed
 Modified

Plugins/TypeChecker/RowTypes/Coxswain
v12 v13 35 35 36 36 {{{ 37 #!haskell38 39 37 {# LANGUAGE BangPatterns #} 40 38 {# LANGUAGE DataKinds #} … … 111 109 ) 112 110 113  Pattern Matching 111  Pattern Matching  TODO: record patterns 114 112 115 113 frag5 !r = … … 124 122 age = r `dot` #age 125 123 126  Updating R ecords124  Updating R Iecords 127 125 128 126 frag7 = ( … … 152 150 prettify rawInput 153 151 154  R ecord Types152  R Iecord Types 155 153 156 154 origin :: R I (Row0 .& "x" .= Float .& "y" .= Float) … … 198 196 Lacks a "name"  Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc. 199 197 , 200 Short (NumCols a + 1)  Merely consequence of particular record implementation.198 Short (NumCols a)  Merely consequence of particular record implemention. 201 199 ) 202 200 => R I (Named a) > String … … 211 209 Lacks a "y" , Lacks a "x"  Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc. 212 210 , 213 Short (NumCols a + 1 + 1)  Merely consequence of particular record implementation.211 Short (NumCols a + 1)  Merely consequence of particular record implemention. 214 212 ) 215 213 => R I (Positioned a) > (Float,Float) … … 223 221 [ getPos origin, getPos dude ] 224 222 225 }}} 226 227 == Beyond Elm 228 229 The current `coxswain` and `sculls` library are capable of more than what's shown in the gentle Elm introduction. This is my current favorite example, a generalization of `partitionEithers`. 230 231 {{{ 232 #!haskell 223  BEYOND THE ELM TUTORIAL 233 224 234 225 vars :: [V I (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)] 235 226 vars = [inj #z True,inj #x 7,inj #y 'h',inj #z False,inj #y 'i',inj #x 3] 236 227 237 pvars :: R (F []) (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool) 238 pvars = partitionVariants vars 228 pvars = vpartition vars 239 229 }}} 240 230 … … 249 239 }}} 250 240 251 The ` partitionVariants` function is not a primitive! The following is its definition inside `sculls`.241 The `vpartition` function is not a primitive! The following is its definition inside `sculls`. 252 242 253 243 {{{ … … 256 246   Partition a list of variants into in listshaped record of the 257 247  same row. 258 partitionVariants :: forall (p :: Row k). Short (NumCols p) => [V I p]> R (F []) p259 partitionVariants= foldr cons (rpure (F []))248 vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p  1)) => f (V I p) > R (F []) p 249 vpartition = foldr cons (rpure (F [])) 260 250 where 261 cons v !acc = elimV (rmap f rHasCol) v251 cons v !acc = velim (f /$\ rhas) v 262 252 where 263 f :: forall (l :: k ) t. (HasCol p :>: I :>: C (R (F []) p)) l t253 f :: forall (l :: kl) t. (HasCol p :>: I :>: C (R (F []) p)) l t 264 254 f = A $ \HasCol > A $ \x > C $ runIdentity $ rlens (Identity . g x) acc 265 255 266 g :: forall (l :: k ) t. I l t > F [] l t > F [] l t256 g :: forall (l :: kl) t. I l t > F [] l t > F [] l t 267 257 g (I x) (F xs) = F (x:xs) 268 258 }}} … … 383 373 In fact, `HasCol p` has that kind, and we'll see below that it can be very useful as a field. 384 374 385 == Back to ` partitionVariants`386 387 Now let's revisit ` partitionVariants` to see those pieces in action with some primitive functions on records and variants.375 == Back to `vpartition` 376 377 Now let's revisit `vpartition` to see those pieces in action with some primitive functions on records and variants. 388 378 389 379 {{{ … … 392 382   Partition a list of variants into in listshaped record of the 393 383  same row. 394 partitionVariants :: forall (p :: Row k). Short (NumCols p) => [V I p]> R (F []) p395 partitionVariants= foldr cons (rpure (F []))384 vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p  1)) => f (V I p) > R (F []) p 385 vpartition = foldr cons (rpure (F [])) 396 386 where 397 cons v !acc = elimV (rmap f rHasCol) v387 cons v !acc = velim (f /$\ rhas) v 398 388 where 399 f :: forall (l :: k ) t. (HasCol p :>: I :>: C (R (F []) p)) l t389 f :: forall (l :: kl) t. (HasCol p :>: I :>: C (R (F []) p)) l t 400 390 f = A $ \HasCol > A $ \x > C $ runIdentity $ rlens (Identity . g x) acc 401 391 402 g :: forall (l :: k ) t. I l t > F [] l t > F [] l t392 g :: forall (l :: kl) t. I l t > F [] l t > F [] l t 403 393 g (I x) (F xs) = F (x:xs) 404 394 }}} … … 422 412 As usual, the objective is for the library to have minimal runtime overhead. With hundreds of `Lacks` constraints floating around, that means  again, as usual  that inlining and specialization are key. Things look promising at this stage. 423 413 424 For example, the ` partitionVariants` example from above (repeating here)414 For example, the `vpartition` example from above (repeating here) 425 415 426 416 {{{ … … 431 421 432 422 pvars :: R (F []) (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool) 433 pvars = partitionVariantsvars423 pvars = vpartition vars 434 424 }}} 435 425 … … 528 518 529 519   Eliminate a variant with a functional record. (Gaster and Jones 1996) 530 elimV:: Short (NumCols p) => R (f :>: C a) p > V f p > a520 velim :: Short (NumCols p) => R (f :>: C a) p > V f p > a 531 521 532 522   Eliminate a record with a functional variant. (Gaster and Jones 1996) 533 elimR:: Short (NumCols p) => V (f :>: C a) p > R f p > a523 relimr :: Short (NumCols p) => V (f :>: C a) p > R f p > a 534 524 535 525   Convert each field to a variant of the same row. 536 variants :: Short (NumCols p) => R f p > R (C (V f p)) p526 rvariants :: Short (NumCols p) => R f p > R (C (V f p)) p 537 527 538 528   Partition a list of variants into in listshaped record of the same row. 539 partitionVariants:: Short (NumCols p) => [V I p] > R (F []) p529 vpartition :: Short (NumCols p) => [V I p] > R (F []) p 540 530 }}} 541 531 … … 561 551 f :: 562 552 ( Lacks r "f" 563 , Short (NumCols r + 1) )553 , Short (NumCols r) ) 564 554 => R I (r .& "f" .= Int) 565 555 > R I (r .& "f" .= Int) … … 581 571   Predicate for supported record sizes. 582 572 class (Applicative (SV n),Traversable (SV n)) => Short (n :: Nat) where 583 select :: SV n a > Fin n> a584 lensSV :: Functor f => (a > f a) > SV n a > Fin n > f (SV na)573 select :: SV (n + 1) a > Fin (n + 1) > a 574 lensSV :: Functor f => (a > f a) > SV (n + 1) a > Fin (n + 1) > f (SV (n + 1) a) 585 575 extend :: SV n a > a > Fin (n + 1) > SV (n + 1) a 586 restrict :: SV (n + 1) a > Fin (n + 1) > (a,SV n a)576 restrict :: SV (n + 1) a > Fin (n + 1) > (a,SV n a) 587 577 indices :: SV n (Fin n) 588 578 }}} 589 579 590 The `SV` data family provides the tuples of `Any` that I currently use to represent records. For example, the `rlens` record primitive is defined by simply coercing the `lensSV` method. I generate `SV` and `Short` instances via Template Haskell. The `SV` instance for ` 3` and its `lensSV` method definition are as follows.580 The `SV` data family provides the tuples of `Any` that I currently use to represent records. For example, the `rlens` record primitive is defined by simply coercing the `lensSV` method. I generate `SV` and `Short` instances via Template Haskell. The `SV` instance for `2` and its `lensSV` method definition are as follows. 591 581 592 582 {{{ … … 596 586 deriving (Foldable,Functor,Show,Traversable) 597 587 598 instance Short 3where588 instance Short 2 where 599 589 ... 600 590 {# INLINE lensSV #}