Changes between Version 12 and Version 13 of Plugins/TypeChecker/RowTypes/Coxswain


Ignore:
Timestamp:
Sep 18, 2017 3:48:15 PM (2 years ago)
Author:
nfrisby
Comment:

update code snippets to match github repo

Legend:

Unmodified
Added
Removed
Modified
  • Plugins/TypeChecker/RowTypes/Coxswain

    v12 v13  
    3535
    3636{{{
    37 #!haskell
    38 
    3937{-# LANGUAGE BangPatterns #-}
    4038{-# LANGUAGE DataKinds #-}
     
    111109  )
    112110
    113 ----- Pattern Matching
     111----- Pattern Matching   -- TODO: record patterns
    114112
    115113frag5 !r =
     
    124122  age = r `dot` #age
    125123
    126 -----  Updating Records
     124-----  Updating R Iecords
    127125
    128126frag7 = (
     
    152150  prettify rawInput
    153151
    154 ----- Record Types
     152----- R Iecord Types
    155153
    156154origin :: R I (Row0 .& "x" .= Float .& "y" .= Float)
     
    198196       Lacks a "name"   -- Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc.
    199197     ,
    200        Short (NumCols a + 1)   -- Merely consequence of particular record implementation.
     198       Short (NumCols a)   -- Merely consequence of particular record implemention.
    201199     )
    202200  => R I (Named a) -> String
     
    211209       Lacks a "y" , Lacks a "x"   -- Necessary difference compared to Elm. Comparable to KnownNat/KnownSymbol/etc.
    212210     ,
    213        Short (NumCols a + 1 + 1)   -- Merely consequence of particular record implementation.
     211       Short (NumCols a + 1)   -- Merely consequence of particular record implemention.
    214212     )
    215213  => R I (Positioned a) -> (Float,Float)
     
    223221  [ getPos origin, getPos dude ]
    224222
    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
    233224
    234225vars :: [V I (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)]
    235226vars = [inj #z True,inj #x 7,inj #y 'h',inj #z False,inj #y 'i',inj #x 3]
    236227
    237 pvars :: R (F []) (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)
    238 pvars = partitionVariants vars
     228pvars = vpartition vars
    239229}}}
    240230
     
    249239}}}
    250240
    251 The `partitionVariants` function is not a primitive! The following is its definition inside `sculls`.
     241The `vpartition` function is not a primitive! The following is its definition inside `sculls`.
    252242
    253243{{{
     
    256246-- | Partition a list of variants into in list-shaped record of the
    257247-- same row.
    258 partitionVariants :: forall (p :: Row k). Short (NumCols p) => [V I p] -> R (F []) p
    259 partitionVariants = foldr cons (rpure (F []))
     248vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p - 1)) => f (V I p) -> R (F []) p
     249vpartition = foldr cons (rpure (F []))
    260250  where
    261   cons v !acc = elimV (rmap f rHasCol) v
     251  cons v !acc = velim (f /$\ rhas) v
    262252    where
    263     f :: forall (l :: k) t. (HasCol p :->: I :->: C (R (F []) p)) l t
     253    f :: forall (l :: kl) t. (HasCol p :->: I :->: C (R (F []) p)) l t
    264254    f = A $ \HasCol -> A $ \x -> C $ runIdentity $ rlens (Identity . g x) acc
    265255
    266   g :: forall (l :: k) t. I l t -> F [] l t -> F [] l t
     256  g :: forall (l :: kl) t. I l t -> F [] l t -> F [] l t
    267257  g (I x) (F xs) = F (x:xs)
    268258}}}
     
    383373In fact, `HasCol p` has that kind, and we'll see below that it can be very useful as a field.
    384374
    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
     377Now let's revisit `vpartition` to see those pieces in action with some primitive functions on records and variants.
    388378
    389379{{{
     
    392382-- | Partition a list of variants into in list-shaped record of the
    393383-- same row.
    394 partitionVariants :: forall (p :: Row k). Short (NumCols p) => [V I p] -> R (F []) p
    395 partitionVariants = foldr cons (rpure (F []))
     384vpartition :: forall (p :: Row kl *) f. (Foldable f,Short (NumCols p),Short (NumCols p - 1)) => f (V I p) -> R (F []) p
     385vpartition = foldr cons (rpure (F []))
    396386  where
    397   cons v !acc = elimV (rmap f rHasCol) v
     387  cons v !acc = velim (f /$\ rhas) v
    398388    where
    399     f :: forall (l :: k) t. (HasCol p :->: I :->: C (R (F []) p)) l t
     389    f :: forall (l :: kl) t. (HasCol p :->: I :->: C (R (F []) p)) l t
    400390    f = A $ \HasCol -> A $ \x -> C $ runIdentity $ rlens (Identity . g x) acc
    401391
    402   g :: forall (l :: k) t. I l t -> F [] l t -> F [] l t
     392  g :: forall (l :: kl) t. I l t -> F [] l t -> F [] l t
    403393  g (I x) (F xs) = F (x:xs)
    404394}}}
     
    422412As usual, the objective is for the library to have minimal run-time 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.
    423413
    424 For example, the `partitionVariants` example from above (repeating here)
     414For example, the `vpartition` example from above (repeating here)
    425415
    426416{{{
     
    431421
    432422pvars :: R (F []) (Row0 .& "x" .= Int .& "y" .= Char .& "z" .= Bool)
    433 pvars = partitionVariants vars
     423pvars = vpartition vars
    434424}}}
    435425
     
    528518
    529519-- | Eliminate a variant with a functional record. (Gaster and Jones 1996)
    530 elimV :: Short (NumCols p) => R (f :->: C a) p -> V f p -> a
     520velim :: Short (NumCols p) => R (f :->: C a) p -> V f p -> a
    531521
    532522-- | Eliminate a record with a functional variant. (Gaster and Jones 1996)
    533 elimR :: Short (NumCols p) => V (f :->: C a) p -> R f p -> a
     523relimr :: Short (NumCols p) => V (f :->: C a) p -> R f p -> a
    534524
    535525-- | Convert each field to a variant of the same row.
    536 variants :: Short (NumCols p) => R f p -> R (C (V f p)) p
     526rvariants :: Short (NumCols p) => R f p -> R (C (V f p)) p
    537527
    538528-- | Partition a list of variants into in list-shaped record of the same row.
    539 partitionVariants :: Short (NumCols p) => [V I p] -> R (F []) p
     529vpartition :: Short (NumCols p) => [V I p] -> R (F []) p
    540530}}}
    541531
     
    561551f ::
    562552    ( Lacks r "f"
    563     , Short (NumCols r + 1) )
     553    , Short (NumCols r) )
    564554  => R I (r .& "f" .= Int)
    565555  -> R I (r .& "f" .= Int)
     
    581571-- | Predicate for supported record sizes.
    582572class (Applicative (SV n),Traversable (SV n)) => Short (n :: Nat) where
    583   select :: SV n a -> Fin n -> a
    584   lensSV :: Functor f => (a -> f a) -> SV n a -> Fin n -> f (SV n a)
     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)
    585575  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)
    587577  indices :: SV n (Fin n)
    588578}}}
    589579
    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.
     580The `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.
    591581
    592582{{{
     
    596586  deriving (Foldable,Functor,Show,Traversable)
    597587
    598 instance Short 3 where
     588instance Short 2 where
    599589  ...
    600590  {-# INLINE lensSV #-}