Skip to content

Instantly share code, notes, and snippets.

@wedens
Created July 19, 2015 04:14
Show Gist options
  • Save wedens/0250c0617150d20a46ba to your computer and use it in GitHub Desktop.
Save wedens/0250c0617150d20a46ba to your computer and use it in GitHub Desktop.
21:14 <edwardk> in scala you could have working coindexed prisms
21:20 <wedens> edwardk: interesting. do you have a gist? is inference the only problem?
21:20 <edwardk> not handy
21:21 <edwardk> the issue is that we want indexed lenses / traversals to downgrade to normal lenses / traversals right?
21:21 <edwardk> well
21:21 <edwardk> to do that (.) unifies 'p' in the second indexed lens you compose with with (->) in the one upstream
21:21 <edwardk> :t traversed
21:21 <lambdabot> (Applicative f1, Traversable f, Indexable Int p) => p a (f1 b) -> f a -> f1 (f b)
21:21 <edwardk> :t traversed.traversed
21:21 <lambdabot> (Applicative f1, Traversable f, Traversable f2, Indexable Int p) => p a (f1 b) -> f (f2 a) -> f1 (f (f2 b))
21:21 <edwardk> this is unification not typeclass based and so does the right thing
21:22 <edwardk> when we start talking about coindexing a prism we'd have the 'p' on the result side not the argument side
21:22 <edwardk> so if you composed a coindexed prism with an indexed lens neither one would determine 'p' except by a bunch of constraints
21:22 <edwardk> and inference goes to hell
21:23 <edwardk> this is why we can't have them in haskell even if we could work through the rest of the profunctor encoding issues
21:23 <wedens> edwardk: what do you think about the whole idea of parsing using lenses? (and getting sensible errors)
21:23 <edwardk> in scala you have to do it all by hand anyways
21:23 <edwardk> wedens: well, that is what they'd be good for
21:24 <edwardk> you'd have to admit slightly improper prisms, since they are merely idempotent
21:24 <edwardk> effectively (ignoring the Maybe noise) parse . pretty . parse = parse
21:25 <edwardk> but we don't have that pretty . parse = id merely that it doesn't lose any information needed for parsing again
21:26 <edwardk> but nothing in the lens library prevents you from working with improper prisms
21:52 <wedens> edwardk: what does coindexed mean?
21:53 <edwardk> well, an indexed lens uses p a (f b) -> s -> f t -- where p can be (->) or it can be Indexed i from "newtype Indexed i a b = Indexed { runIndexed :: i -> a -> b }
21:54 <edwardk> a coindexed prism would use (a -> f b) -> p s (f t) -- for a p that can be (->) or it can be newtype Coindexed i a b = Coindexed { runCoindexed :: a -> Either i b }
21:55 <edwardk> the 'i' or 'coindex' is 'what information you can fail with'
21:55 <edwardk> now that is sadly too simplistic
21:55 <edwardk> because it misses the rest of the prism structure
21:55 <edwardk> but that'd be a coindexed lens
21:55 <edwardk> or rather a coindexed affine traversal or something
21:56 <edwardk> having the 'f' in there mucks everything up for symmetry
21:56 <edwardk> and not having it mucks up presenting indices/coindices, so there is an awkward representation problem
21:57 <edwardk> anyways coindexed is possibly a bad name
21:57 <edwardk> but its the one we thought of when i started playing with it
21:58 <edwardk> if you tease apart indexed to make it into (i * a) -> b then this is a -> (i + b)
21:58 <edwardk> it has fewer nice properties than the former, since we can shove the 'i' in the former to either side of the (->), but it is still interesting.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment