-XApplyingVia — sort @(Int via Down Int) #218
-XApplyingVia — sort @(Int via Down Int) #218Icelandjack wants to merge 2 commits intoghc-proposals:masterfrom
Conversation
|
This replaces some use cases for |
|
Cool, I like this! |
|
Thanks man, I would love to find more examples compositions; here is one I found on IRC >> (($ "") . appEndo . getConst . traverse (\x -> Const (Endo (x:)))) "hello"
"hello"
>> traverse @_ @(String -> String via Const (Endo String) _) (:) "hello" ""
"hello"
>> traverse @_ @(via Const . Endo) (:) "hello" "" |
|
Would this allow us to break the invariants guaranteed by global instance coherence? For example, would I be allowed to write the following? s :: Set Int
insert @(Int via Down Int) s 5It seems that your suggestion is to desugar coerce (insert @(Down Int)) s 5I would hope that the work on roles and safe coercions would save us here, and indeed it does. ghci> coerce @(Down Int -> Set (Down Int) -> Set (Down Int)) @(Int -> Set Int -> Set Int) insert s 5
<interactive>:1:1: error:
• Couldn't match type ‘Down Int’ with ‘Int’
arising from a use of ‘coerce’
• In the expression:
coerce
@(Down Int -> Set (Down Int) -> Set (Down Int))
@(Int -> Set Int -> Set Int)
insert
s
5The proposal should address this potential issue, alongside other fleshing out (like specifying what the desugaring plan is :) |
|
Interesting idea, worthwhile exploring! (shameless plug) reminds me of https://www.reddit.com/r/haskell/comments/765ogm/multiple_type_class_instances_for_the_same_type/doc8enp/ |
|
Vote for names: |
|
Vote for names: |
|
Given data Fold :: Type -> Type -> Type where
Fold :: Monoid mm
=> { tally :: a -> mm
, summarize :: mm -> b
}
-> Fold a bWe might want our |
|
I like this idea, and think it's definitely worth exploring further here! The fact that |
|
@iamrecursion Thank you! It is exciting @gridaphobe This is based on It works with >> insert @(Int via Down Int) 0 [1..4]
[1,2,3,4,0]
>>
>> (coerce $ insert @(Down Int) :: Int -> [Int] -> [Int]) 0 [1..4]
[1,2,3,4,0]funky 🤐 I would appreciate help establishing a clear semantics and desugaring @nomeata Thanks, it's all built on your work on |
|
So the idea is that fun :: forall a. F(a)
fun @(X via Y)is instantiated to F(Y) and then coerced to F(X), correct? What does this do if some constraints depend on and aren't satisfied by Y? Would they remain as constraints on Y? example :: forall s m . (MonadState s m, IsList s, Ord s) => ...
example' = example @(Int via Down Int)should example' be forall m . (MonadState (Down Int) m, IsList (Down Int), Ord (Down Int)) => ...
-- Ord (Down Int) is solved, of course, and in the general case Ord (Down a) would become (Ord a)Edit: If this is the behaviour it would be something more like: fun :: forall a. C(a) => F(a)
fun @(X via Y) :: C(Y) => F(X) |
|
I'm a little uneasy with it. Deriving via introduced codegen in a context where we were already doing codegen (the deriving mechanism). Applying via introduces codegen in a place where it was not found previously (type application). I think instead of type coercions, what I actually want to see is something like explicit typeclass dictionary applications. So if the function calls for (Ord a) I want to be able to say "sort @(Ord a via Down a)". (Insert much handwaving here about how to tell which "a" is intended if there are multiple Ord constraints). I am more able to wrap my head around what this does, because it's just choosing a different typeclass dictionary to pass to the function. Of course this is a Bad Idea to do with Data.Set functions. Perhaps that detail should be addressed in this proposal as well? |
|
Why do you call this codegen @DanBurton? Coercing |
|
Despite its being extraordinarily useful, I've never loved deriving-via, essentially for the reasons @DanBurton describes. The key trick in deriving-via is to use newtypes to stand in for named instances. Clever use of A case in point is a recent usage of deriving-via: A class I wanted instances of didn't have the right generic default for my purposes. So I wrote a newtype, an instance for that newtype, and then used a lot of deriving-via. But I'd much rather have done this without the newtype (which wasn't otherwise useful): if I could name the instance directly, then this would be simpler. One could argue that the newtype acts as the name of an instance, and that one would be right -- but again, let's not have play-acting: let's just name the instance. This proposal (which I think holds water and may prove to be just as useful in practice as deriving-via) expands our use of newtypes as proxies for named instances. As an alternative, I'd love to consider Coherent Explicit Dictionary Application for Haskell by Thomas Winant and Dominique Devriese. I liked the presentation at last year's Haskell Symposium, but I haven't studied this in detail. Would it lead to a cleaner way to do all this? |
|
I call it "codegen" because it is basically a macro to insert "coerce" at certain points in the code. Coerce might have 0 runtime cost, but it is still "code" with a semantic meaning. Reflecting on this, I should state one further cause for unease, which is that type applications have historically served only to "narrow" the type of a function call. Erasing the type application will either a) be inferred to the same type, or b) be too ambiguous to infer. ApplyingVia allows type applications to change the type of a function call, so that erasing the type application c) changes the behavior of the code. It may be worthwhile to do, but it is something that type applications have not been able to do before. If turning on this extension means that type applications cannot be "safely erased", then this is worth noting. (Define "safely erased" to mean "either a) the code runs the same, or b) it fails to compile"; the latter being a more tedious case to deal with, but still "safe" in the sense that you don't end up with different runtime code.) |
I don't have a precise definition in mind, I just have a few reference points.
So what I'm saying is, if you're going to make a case for ApplyingVia, then there should be some attempt at comparing/contrasting the other points in the design space for similar features. In this case, that would be Coherent Explicit Dictionary Application for Haskell, as mentioned by @goldfirere (which I have not yet reviewed but it sounds like exactly what I'm picturing). I'd also love to see a more explicit comparison/contrast to |
This is presumably part of the continuing campaign to make Haskell indistinguishable from line noise. Please stop with the hier@glyphics already. What's become of the succinct yet readable, elegant language by which I came to love functional programming? Is this intended merely as a shorthand for something I could write today? From the proposal's "(handwave)" I'm not seeing what; so I can't see what all those Is there any benefit for users of packages as opposed to writers of packages? Will users get faced with these hier@glyphics (perhaps in error messages)? I'm experiencing that GHC today with all its extensions is just too big of a language to be usable. The language is in danger of disappearing up its categorial fundament. |
|
I'll make time to address comments about names and what that entails later. @AntC2: Thanks for sharing your opinions. The notation fits my view of Haskell,
Yes a shorthand for Not limited to library authors. Doesn't appear in error messages. |
|
|
I will describe Coherent Explicit Dictionary Application (CEDA from here on) and its approach. It's a good paper and these are my preliminary observations. There is an obvious appeal of exposing dictionaries to users as CEDA does, a case-insensitive What does CEDA entail? We generate a newtype Eq.Dict a = Eq.Dict { (==) :: a -> a -> Bool }
data Ord.Dict a = Ord.Dict { parent1 :: Eq.Dict a, (<=) :: a -> a -> Bool }fields named class (Num a, Ord a) => Real a ..
-- to
class (Ord a, Num a) => Real a ..(I assume the order in which methods are declared matters in the same way, this would be nice with row types!) The design of CEDA does not support associated types and data Eq.Dict a = Eq.Dict { (==) :: a -> a -> Bool, (/=) :: a -> a -> Bool }
data Ord.Dict a = Ord.Dict { parent1 :: Eq.Dict a, compare :: a -> a -> Ordering, (<) :: a -> a -> Bool, (<=) :: a -> a -> Bool, (>) :: a -> a -> Bool, (>=) :: a -> a -> Bool, max :: a -> a -> a, min :: a -> a -> a }CEDA recommends writing smart constructors, and case-insensitive smartEq :: (a -> a -> Bool) -> Eq.Dict a
smartEq (===) = Eq.Dict { (==) = (===), (/=) = \a b -> not (a === b) }
nub @{ smartEq (\str str' -> map toLower str == map toLower str') }They optionally propose a special constraint to get the dictionary for a given type, whose instances are generated by the compiler class HasDict (c :: Constraint) where
type DictOf c :: Type
getDict :: c => DictOf cto avoid writing Ord.Dict
{ parent1 = Eq.Dict
{ (==) = (==)
, (/=) = (/=)
}
, compare = compare
, (<) = (<)
, (<=) = (<=)
, (>) = (>)
, (>=) = (>=)
, max = max
, min = min
}If we have a function with two constraints of the same type class foo :: (Eq a, Eq b) => (a, b) -> (a, b) -> ..how do we override only That is a big proposal with many choices, it requires compiler generated dictionaries and optional compiler generated constraint where superclass, method order and alpha-equivalent types start to matter.
Because it is type-directed rather than dictionary-directed we never need to disambiguate between constraints (we do need a type signature for foo :: forall a b. (Eq a, Eq b) => (a, b) -> (a, b) -> ..since type variables are already ordered: There are some other questions but I'm tired so I won't answer them right now! Idk not really a conclusion |
|
As I'm thinking about this more, I'm not sure what the exact specification of this would be. I thought we would treat So then we can say that But what if more specified variables intervene? Then the maximal instantiation trick doesn't work. And what if there are class constraints that mention multiple variables? It's not quite clear to me. So I think we might need a full specification before going much further... (By the way, many thanks for the summary and analysis of CEDA w.r.t. this proposal. Very helpful!) |
|
similarly we could write newtype Const a b = Const a
instance Functor (Const a) where
fmap :: (b -> b') -> (Const a b -> Const a b')
fmap _ (Const a) = Const a
instance Monoid a => Applicative (Const a) where
pure :: b -> Const a b
pure _ = Const mempty
(<*>) :: Const a (b -> b') -> Const a b -> Const a b'
Const a <*> Const a' = Const (a <> a') as instance Functor (Const a via a) where
fmap :: (b -> b') -> (a -> a)
fmap _ = id
instance Monoid a => Applicative (Const a via a) where
pure :: b -> a
pure _ = mempty
(<*>) :: a -> a -> a
(<*>) = (<>) |
|
An observation nub :: forall a. Eq a => [a] -> [a]
nubOrd :: forall a. Ord a => [a] -> [a]
nubHash :: forall a. Hashable a => Eq a => [a] -> [a]CEDA is dictionary-based, we cannot change the underlying function to one with different constraints without updating the dictionary to agree. Now we are hoist by the necessity to construct and name dictionaries (maybe you want to vary them separately?), same wth nub @{eqCaseInsensitive}
nubOrd @{ordCaseInsensitive}
nubHash @{hashCaseInsensitive} @{eqCaseInsensitive}
liftM @{myMonad}
liftA @{parent1 myMonad}
fmap @{parent1 (parent1 myMonad)}The type-focused nub @(String via CaseInsensitive)
nubOrd @(String via CaseInsensitive)
nubHash @(String via CaseInsensitive)
liftM @(m via My m)
liftA @(m via My m)
fmap @(m via My m)
CEDA does not mean that a single name replaces the module CEDA (eqCaseInsensitive, ordCaseInsensitive, hashCaseInsensitive, ..) |
|
I'm not so worried about the covariance between function name and dictionary name in CEDA. We could always have a way of abstracting over that, by (say) having a class that classifies dictionary types, so the correct dictionary could be selected in a type-directed fashion. |
|
The show stopper for (\@m -> traverse @_ @(m via Const m))
:: Traversable t => Monoid m => (a -> m) -> (t a -> m)What about via traverse @_ @(?? via Identity)
:: Traversable t => (a -> b) -> (t a -> t b)If all uses of the Applicative functor traverse @_ @(forall x. x via Identity x)
type Id a = a
traverse @_ @(Id via Identity)
type family Id a where Id a = a
traverse @_ @(Id via Identity)
traverse @_ @((\x -> x) via Identity)but I'm not happy with those designs :) just putting it out there |
|
This cool implementation of a SAT solver https://julesh.com/2016/09/22/abusing-the-continuation-monad/, the idea to replace sat :: Int -> ([Bool] -> Bool) -> Bool
sat n = runCont $ replicateM n $ cont $ \k -> k True || k FalseHere it is in longer form with no sat n = replicateM @(forall x. (x -> Bool) -> Bool via Cont Bool x) n $ \k -> k True || k False
type Cont_ res a = ((a -> res) -> res)
sat n = replicateM @(Cont_ Bool via Cont Bool) n $ \k -> k True || k False |
|
Keeping track of examples. >> sequenceA @[] @[] ["ABC", "123", "!"]
["A1!","A2!","A3!","B1!","B2!","B3!","C1!","C2!","C3!"]
>> sequence @([] via ZipList) @[] ["ABC", "123", "!"]
["A1!","A2!","A3!","B1!","B2!","B3!","C1!","C2!","C3!"]
>> sequence @[] @([] via ZipList) ["ABC", "123", "!"]
["A1!"]
>> sequence @([] via ZipList) @([] via ZipList) ["ABC", "123", "!"]
["A1!"]Accumulating sum (and >> foldMap @[] @((Float, Int) via (Sum Float, Sum Int)) (,1) [pi, pi, pi]
(9.424778,3)
>> import Debug.SimpleReflect
>>
>> foldMap @[] @Expr realFrac [pi,pi,pi]
3.1415927410125732 <> 3.1415927410125732 <> 3.1415927410125732 <> mempty
>> foldMap @[] @(Expr via Dual Expr) realFrac [pi,pi,pi]
((mempty <> 3.1415927410125732) <> 3.1415927410125732) <> 3.1415927410125732
>> foldMap @[] @((Float,Expr,Int) via (Sum Float,Expr,Sum Int)) (\fl -> (fl, realToFrac fl,1) [pi, pi, pi]
(9.424778,3.1415927410125732 <> 3.1415927410125732 <> 3.1415927410125732 <> mempty,3)instance Folding M where
run s (M k h m (z :: m)) = reify (m, z) $
\ (_ :: Proxy s) -> k $ runN (foldMap (N #. h) s :: N m s)
-- becomes (and avoids reify with DH)
instance Folding M where
run s (M k h m (z :: m)) = reify (m, z) $
\ (_ :: Proxy s) -> k $ foldMap @_ @(m via N_ m s) h sfoldMapA :: forall t f a b. (Foldable t, Applicative f, Monoid b) => (a -> f b) -> (t a -> f b)
foldMapA f = getAp . foldMap (Ap . f)
-- becomes
foldMapA :: forall t f a b. (Foldable t, Applicative f, Monoid b) => (a -> f b) -> (t a -> f b)
foldMapA = foldMap @_ @(b via Ap f b)bind :: forall f a. Traversable f => f a -> (f (Kahn a), (Int,Int))
bind as = (r,(0,hi)) where
r :: f (Kahn a)
hi :: Int
(r,hi) = runState (mapM freshVar as) 0
freshVar :: a -> State Int (Kahn a)
freshVar a = state $ \s -> let s' = s + 1 in s' `seq` (var a s, s')
--
bind :: forall f a. Traversable f => f a -> (f (Kahn a), (Int, Int))
bind as = (r,(0,hi)) where
r :: f (Kahn a)
hi :: Int
(r,hi) = mapM @_ @(Int -> (a, Int) via State Int a)
freshVar as 0
freshVar :: a -> Int -> (Kahn a, Int)
freshVar a s = let s' = s + 1 in s' `seq` (var a s, s')mapAccumL f s t = runStateL (traverse (StateL . flip f) t) s
mapAccumR f s t = runStateR (traverse (StateR . flip f) t) s
mapAccumL = flip . traverse' @(forall x. a -> (a, x) via StateL a x) . flip
mapAccumR = flip . traverse' @(forall x. a -> (a, x) via StateR a x) . flipfrom irc, although I prefer the locality it shouldn't be this much longer > replicateM 3 (StateT (reads :: ReadS Integer)) `runStateT` "12 13 14"
[([12,13,14],"")]
> replicateM @(String -> [(a, String)] via via StateT String [] a) 3 (reads @Integer) "12 13 14"
[([12,13,14],"")]mapConcurrently :: Traversable t => (a -> IO b) -> t a -> IO (t b)
mapConcurrently = traverse @_ @(IO via Concurrently)
mapConcurrently_ :: Foldable f => (a -> IO b) -> f a -> IO ()
mapConcurrently_ = traverse_ @_ @(IO via Concurrently)
replicateConcurrently :: Int -> IO a -> IO [a]
replicateConcurrently = replicateM @(IO via Concurrently)
replicateConcurrently_ :: Int -> IO a -> IO ()
replicateConcurrently_ n = replicateM_ @(IO via Concurrently)irc >> :t getCompose .: traverse @[] @(Compose IO (Either _)) . fmap Compose
.. :: (a -> IO (Either err b)) -> [a] -> IO (Either err [b])
>> :t \@err -> traverse @[] @(forall x. IO (Either err x) via Compose IO (Either err) x)
.. :: (a -> IO (Either err b)) -> [a] -> IO (Either err [b])Löb löb :: Functor f => f (f a -> a) -> f a
löb funs = fix (\fs -> fmap ($ fs) funs)
löb @(forall r a. ((a -> r) -> r) via Cont r a)
:: (((((a -> r) -> r) -> a) -> r) -> r) -> ((a -> r) -> r)
-- better solution:
löb @(via cont)
:: (((((a -> r) -> r) -> a) -> r) -> r) -> ((a -> r) -> r)I noticed
So we wanted to use the functionality of lift :: forall f a b n. Applicative f => Applyable b n => (a -> b) -> (f a -> AppFunc n f b)
>> lift @[] (+) [1, 2] [10, 20]
[11,21,12,22]
>> lift @ZipList (+) (ZipList [1, 2]) (ZipList [10, 20])
ZipList {getZipList = [11,22]}Due to the incompleteness we cannot apply it to but we happen to know this holds right? well, if we did we should have the option of gzipWith = lift @([] unsafe via ZipList)memoizeFinite :: forall a. Enum a => Bounded a => (a -> b) -> (a -> b)
memoizeFinite = memoize @(a via Finite a)A lot of cool impredicative examples, using experimental syntax pure @(via! Yoneda @Identity) :: a -> forall res. (a -> res) -> res
pure @(via! Codensity @Identity) :: a -> forall res. (a -> res) -> res
pure @(via! Yoneda @((->) b)) :: a -> forall res. (a -> res) -> (b -> res)
pure @(via! Codensity @((->) b)) :: a -> forall res. (a -> (b -> res)) -> (b -> res)
fmap @(via! Yoneda @Endo) :: (a -> b) -> ((forall x. (a -> x) -> (x -> x)) -> (forall y. (b -> y) -> (y -> y)))
fmap @(via! Ran @Identity @Endo) :: (a -> b) -> ((forall x. (a -> x) -> (x -> x)) -> (forall y. (b -> y) -> (y -> y)))
fmap @(via! Codensity @Endo) :: (a -> b) -> ((forall x. (a -> (x -> x)) -> (x -> x)) -> (forall y. (b -> (y -> y)) -> (y -> y)))from lens beside l r f = tabulate $ getCompose #. bitraverse (Compose #. sieve (l f)) (Compose #. sieve (r f))
beside l r f = tabulate $ bitraverse @_ @(via Compose @(Rep q) @f) (sieve (l f)) (sieve (r f))pad :: String -> Int -> String
pad str n = str <|> @(via ZipList) replicate n ' 'QuickCheck: >> sample $ arbitrary @(via ASCIIString)
""
"^"
"U_\FS"
"qG\DC2F~"
"hR]=6"
"\US\ETXL\DLE%aK E"
" \DLE,pDK\NUL@~\EOT5$"
")\fTB\DC3)\RSD%_UDbH"
"\SI\v K\\"
"P"
"\GS+'f1^Uu<"
>> sample $ arbitrary @([[Int]] via OrderedList (NonEmptyList (Positive (Large Int))))
[]
[[1]]
[[5,8,6,5],[6,6,8]]
[[1,5],[1,15,15,14],[7,10,3,2,16],[10,13,5,11],[11,13,9,16],[16,10,4,8]]
[[8,62,7,26,20,14],[35,41,25,56,28],[77,80,109,107,103,42],[78,78,70,125,104,36]]
..newtype ArbitraryEnum a = ArbitraryEnum a deriving newtype (Bounded, Enum)
newtype ArbitraryFractional a = ArbitraryFractional a deriving newtype (Num, Fractional)
instance (Bounded a, Enum a) => Arbitrary (ArbitraryEnum a) where
arbitrary :: Gen (ArbitraryEnum a)
arbitrary = arbitraryBoundedEnum
instance Fractional a => Arbitrary (ArbitraryFractional a) where
arbitrary :: Gen (ArbitraryFractional a)
arbitrary = arbitrarySizedFractional
>> data B = F | T deriving stock (Show, Bounded, Enum)
>>
>> sample $ arbitrary @(via ArbitraryEnum)
T
F
..
>> newtype FLOAT = FLOAT Float deriving stock (Show) deriving newtype (Num, Fractional)
>>
>> sample $ arbitrary @(via ArbitraryFractional)
FLOAT 0.0
FLOAT (-2.2061577)
FLOAT 13.428107
FLOAT 3.4943657
FLOAT (-9.44709)
FLOAT 1.1487609
FLOAT 12.563746
FLOAT 4.5106926
FLOAT (-10.366447)
FLOAT (-16.974293)
FLOAT 26.306278>> import Control.Applicative.Backwards
>>
>> sequenceA [Left 1, Left 2]
Left 1
>> sequenceA @_ @(via Backwards) [Left 1, Left 2]
Left 2newtype Op cat a b = Op { getOp :: cat b a }
instance Category cat => Category (via getOp) where
id :: cat a a
id = id
(.) :: cat b c -> cat a b -> cat a c
(.) = flip (.)
(>>>) :: Category cat => cat a b -> cat b c -> cat a c
(>>>) = (.) @(via Op)Cute :] ($) :: (a -> b) -> (a -> b)
($) = (<$>) @(via Identity)
= (<*>) @(via Identity)
= (=<<) @(via Identity)
= traverse @(via Identity) @(via Identity)
= (=<<<) @(via IdentityT) @(via Identity)
(&) :: a -> (a -> b) -> b
(&) = (<&>) @(via Identity)
= (<**>) @(via Identity)
= (>>=) @(via Identity)
= for @(via Identity) @(via Identity)
= (>>>=) @(via IdentityT) @(via Identity)
id :: a -> a
id = pure @(via Identity)
= join @(via Identity)
= (??) @(via Identity)
= fmap @(via Const) not
= contramap @(via Const) (+ 1)
= lift @(via IdentityT) @(via Identity)
= (() <$ @(via Const))
= ($> @(via Const) ())
const :: a -> b -> a
const = (<$) @(via Identity)
= ($>) @(via Const)
= ($<) @(via Const)
flip const :: b -> a -> a
flip const = ($>) @(via Identity)
= (<$) @(via Const)
= (>$) @(via Const)
mempty :: Monoid m => m
mempty = pure @(via Const) ()
= fold @(via Const) ()
= traverse @(via Const) not "abc"
mappend :: Monoid m => m -> m -> m
mappend = (<*>) @(via Const)
fmap :: (a -> b) -> Functor f => (f a -> f b)
fmap = collect @(via Identity)
test :: (a -> Bool) -> (a -> Maybe a)
test = find @(via Identity)
filter :: (a -> Bool) -> ([a] -> [a])
filter = filterM @(via Identity)
fix :: (a -> a) -> a
fix = mfix @(via Identity)
cycle :: Monoid m => m -> m
cycle = forever @(via Const)
replicate :: Int -> a -> [a]
replicate = replicateM @(via Identity)
mtimes :: Int -> Monoid m => m -> m
mtimes = replicateM @(via Const)
= replicateM_ @(via Const)
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(>=>) = (>>>) @(via Kleisli)
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)
(<=<) = (<<<) @(via Kleisli)
(\case True -> id; False -> const mempty) :: Bool -> Monoid m => m -> m
(\case True -> id; False -> const mempty) = when @(via Const)
(\case True -> const mempty; False -> id) :: Bool -> Monoid m => m -> m
(\case True -> const mempty; False -> id) = unless @(via Const)
foldMap :: Monoid m => (a -> m) -> ([a] -> m)
foldMap = filterM @(via Const)
ifoldMap @_ @(via Identity)
:: Monoid m => (() -> a -> m) -> (a -> m)example from Justin Le, here the via proxy gets too complicated; what to do -- changes underlying state, like zoom from lens
overStateT :: Functor m => (t -> s) -> (s -> t) -> (StateT s m a -> StateT t m a)
overStateT = dimap @(via Star . (Compose .) . runStateT)
transpose :: [[a]] -> [[a]]
transpose = sequenceA @[] @(via ZipList)-- like we have
>> filterM @[] (const [False, True]) [1..3]
[[],[3],[2],[2,3],[1],[1,3],[1,2],[1,2,3]]
-- has anyone used it with ZipList
>> filterM @(via ZipList) (\a -> ['1' `elem` show a, even a, odd a]) [1..10]
[[1,10],[2,4,6,8,10],[1,3,5,7,9]]>> guard @[] True
[()]
>> guard @[] False
[]
>> guard @(via ZipList) True
repeat ()
>> guard @(via ZipList) False
[]>> replicateM @(via ZipList) 10 "Earth"
["EEEEEEEEEE","aaaaaaaaaa","rrrrrrrrrr","tttttttttt","hhhhhhhhhh"]
>> zipWithM (via ZipList) (\a b -> [take a b, drop a b]) [1..3] ["ABC", "abc", "!?#"]
[["A","ab","!?#"],["BC","c",""]]Function instance for numbers, via >> (negate + @(via Ap) negate) 10
-20At this point I would favour the original notation, there may be a better notation >> mconcat @([Int] via ZipList `Ap` Sum Int) [ [1..4], [10,20,30], [100,200] ]
[111, 222]
>> mconcat @(via Ap . ZipList . map Sum) [ [1..4], [10,20,30], [100,200] ]
[111, 222]
>> mconcat @([Int] via [] `Ap` Sum Int) [[1,2,3,4], [10,20,30], [100,200]]
[111,211,121,221,131,231,112,212,122,222,132,232,113,213,123,223,133,233,114,214,124,224,134,234]
>> mconcat @(via Ap . map Sum) [[1,2,3,4], [10,20,30], [100,200]]
[111,211,121,221,131,231,112,212,122,222,132,232,113,213,123,223,133,233,114,214,124,224,134,234]
>> optional @[] "hello"
[Just 'h',Just 'e',Just 'l',Just 'l',Just 'o',Nothing]
>> optional @(via ZipList) "hello"
[Just 'h',Just 'e',Just 'l',Just 'l',Just 'o',Nothing,Nothing,Nothing,Nothing,No
asum :: Foldable t => Alternative f => t (f a) -> f a
asum = mconcat @(via Alt)
>> asum @[] @ZipList (words "H -e --l ---l ----o -----!")
"Hello!"
>> mconcat @(via Alt . ZipList) (words "H -e --l ---l ----o -----!")
"Hello!"
>> :set +m
>> let
>| (<·>) :: Applicative f => [f a] -> [f a] -> [f a]
>| (<·>) = (<|>) @(via Compose @ZipList)
>|
>> words "HELLO" <·> words "- my" <·> words "- - BEST" <·> words "- - - !"
["HELLO","my","BEST","!"]reverse :: [a] -> [a]
reverse = foldMap @[] @(via Dual) pure
= toList @(via Reverse)-- Find from end-to-front
>> find @(via Reverse) even [100, 1,3,5,7,9, 2]
Just 2
-- Print in reverse
>> for_ @(via Reverse) [1..5] print
5
4
3
2
1
-- Print in reverse, concurrently
>> for_ @(via Reverse) @(via Concurrently) [1..5] print
5
4
3
21
-- if we omit $! the thunk of `product [1..30000]` would win without any work
>> asum @(via Concurrently) [pure $! product [1..30000], pure $! 2, pure $! product [1..30000] ]
2> asum @[] @(via ZipList) $ words "g -e --t -u p"
"get"
> asum @(via Reverse) @(via ZipList) $ words "g -e --t -u p"
"put"eq (Leibniz equality) newtype a:=b = Refl { subst :: forall ctx. ctx a -> ctx b }
castWith :: (a := b) -> (a -> b)
castWith (Refl eq) = eq @(via Identity)
symm :: (a := b) -> (b := a)
symm (Refl eq) = eq @(via Data.Bifunctor.Flip.Flip)
newtype Lift f a a' = Lift (f a := f a')
lift :: (a := a') -> (f a := f a')
lift (Ref eq) = eq @(via Lift) id
runAp_ :: Monoid m => (forall a. f a -> m) -> Ap f b -> m
runAp_ = runAp @(via! Const)maximum = minimum @_ @(via Down)
-- or
minimum = maximum @_ @(via Down)
class Eq a => Ord a where
..
min, max :: a -> a -> a
min = max @(via Down)
max = min @(via Down)Showing >> print [1..3]
[1,2,3]
>> print ['a','b','c']
"abc"
newtype Lit = MkLit { unLit :: Char }
instance Show Lit where
showsPrec :: Int -> Lit -> ShowS
showsPrec = showsPrec @(via unLit)
-- default 'showList :: [Lit] -> ShowS' implementation
>> print @(String via [Lit]) ['a','b','c']
['a','b','c']
>> print @(via map MkLit) ['a','b','c']
['a','b','c']>> print @(via map Lisp) [1..8]
'(1 2 3 4 5 6 7 8)
>> print @(forall a. [[a]] -> [Lisp [Lisp a]]) [[1],[2],[3],[4]]
'('(1) '(2) '(3) '(4))
>> print @(via lispify) [[1],[2],[3],[4]]
'('(1) '(2) '(3) '(4))
newtype Lisp a = Lisp { unLisp :: a }
instance Show a => Show (Lisp a) where
showsPrec :: Int -> Lisp a -> ShowS
showsPrec = showsPrec @(via unLisp)
showList :: [Lisp a] -> ShowS
showList [] end = "'()" ++ end
showList (x:xs) end = '\'' : '(' : shows x (showl xs) where
showl :: [Lisp a] -> String
showl [] = ')' : end
showl (a:as) = ' ' : shows a (showl as)
type Via = Coercion
pattern Via = Coercion
lispify :: [[a]] `Via` [Lisp [Lisp a]]
lispify = Via
can be formulated in terms of
newtype Baz t b a = Baz { runBaz :: forall f. Applicative f => (a -> f b) -> f t }
sold :: Baz t a a -> t
sold (Baz baz) = baz @(via Identity) id
instance Traversable (Baz t b) where
traverse :: forall f a a'. Applicative f => (a -> f a') -> (Baz t b a -> f (Baz t b a'))
traverse f (Baz baz) = bizarre <$> baz @(via Compose) (fmap sell . f) where
bizarre :: Bazaar a' b t -> Baz t b a'
bizarre = coerce
instance Traversing (->) where
wander :: forall a b s t. (forall f. Applicative f => (a -> f b) -> (s -> f t)) -> (a -> b) -> (s -> t)
wander traverse = traverse @(via! Identity)
-- Note that we are using via from both sides, we go from
--
-- a -> WrappedMonad m b
-- a -> m b
-- Kleisli m a b
instance Monad m => Traversing (runKleisli @m) where
wander :: forall a b s t. (forall f. Applicative f => (a -> f b) -> (s -> f t)) -> ((a -> m b) -> (s -> m t))
wander traverse = traverse @(via! WrappedMonad)
instance Profunctor p => Traversing (via runCofreeTraversing @pro) where
traverse' p = p @(via! Compose)we can also rewrite the laws dimap Compose getCompose . traverse' ≡ traverse' . traverse'
dimap Identity runIdentity . traverse' ≡ idwith traverse' @(via! Compose) ≡ traverse' . traverse'
traverse' @(via! Identity) ≡ idliftR2 :: Representable f => (a -> b -> c) -> (f a -> f b -> f c)
liftR3 :: Representable f => (a -> b -> c -> d) -> (f a -> f b -> f c -> f d)
liftR2 f fa fb = tabulate $ \i -> f (index fa i) (index fb i)
liftR3 f fa fb fc = tabulate $ \i -> f (index fa i) (index fb i) (index fc i)
-- becomes
liftR2 = liftA2 @(via Co)
liftR3 = liftA3 @(via Co)Newly added, map1 :: Functor1 ho => (f ~> f') -> (ho f -> ho f')
map1 @(via Applied) :: => (f ~> f') -> (f ~> f')
fmapRep :: forall f a b. Representable f => (a -> b) -> (f a -> f b)
fmapRep f = cotraverse1 @_ @(via Applied) (f . runIdentity)
cotraverseRep :: Representable r => Functor f => (f a -> b) -> (f (r a) -> r b)
cotraverseRep f = cotraverse1 @_ @(via Composed) (f . fmap runIdentity)
distributeNap :: Representable f => Functor w => w (f a) -> f (w a)
distributeNap = cotraverse1 @_ @(via Composed) (fmap runIdentity)Laws are fruitful: distribute1 . Applied ≡ fmap (Applied . Identity)Functors representational in their first argument could be written distribute1 @_ @(via Applied) = fmap Identityor relating to dist1 :: forall f ho identity. Identity ~ identity => Representative f => Functor1 ho => ho f -> f (ho identity)
dist1 = distribute1waitPrint :: Int -> IO ()
waitPrint n = do
threadDelay n
print n
microsecs :: [Int]
microsecs = [9000,2000,3000,4000,5000,8000]
>> foldMap waitPrint microsecs
9000
2000
3000
4000
5000
8000
>> foldMap @_ @(via Concurrently) waitPrint microsecs
2000
3000
4000
5000
9080000
0
>> foldMap @_ @(via Alt . Concurrently) waitPrint microsecs -- this uses 'race'! 2000 milliseconds runs first
2000 |
Is there a way to leverage inference so that this doesn't require such verbosity (or a type alias)? So that you can write something like: What if the type application and the via application could be written side-by-side instead? And then the type could be omitted |
|
One reason I'm inclined to nudge the proposal in this direction is that it may help distinguish Via Applications as a separate sort of thing, rather than being a new special case in the "type" space. |
The information we want to convey is cont :: forall a r. ((a -> r) -> r) -> Cont r aThe way
We can do the same where replicateM @(Cont Bool) :: Int -> Cont Bool a -> Cont Bool [a]
replicateM @(via cont @_ @Bool) :: Int -> ((a -> Bool) -> Bool) -> (([a] -> Bool) -> Bool)The sat :: Int -> ([Bool] -> Bool) -> Bool
sat n = replicateM @(via cont) n (\k -> k True || k False)Similarly it could work for any "proxy" |
|
Using the same value-level witness for instance declarations, it would probably be the other way round runContT :: ContT r m a -> ((a -> m r) -> m r)note: the body of instance Functor (via runContT @k @r @m) where
fmap :: (a -> a') -> (((a -> m r) -> m r) -> ((a' -> m r) -> m r))
fmap = flip (.) . flip (.)
instance Semigroup (via getAny) where
(<>) :: Bool -> Bool -> Bool
(<>) = (||)
instance Monoid (via getAny) where
mempty :: Bool
mempty = False |
|
(proxy means |
import Data.Semigroup renaming
( (+) from (<>) @(via Sum)
, (*) from (<>) @(via Product)
, (&&) from (<>) @(via All)
, (||) from (<>) @(via Any)
, (<|>) from (<>) @(via Alt)
, union from (<>) @(Set _)
, union' from (<>) @(Map _ _)
, const from (<>) @(via First)
, tsnoc from (<>) @(via Last)
, liftS from (<>) @(via Ap)
)
import Data.Foldable renaming
( mapConcurrently_ from traverse_ @_ @(via Concurrently) )
import Data.Traversable renaming
( mapConcurrently from traverse @_ @(via Concurrently) )
import Control.Monad renaming
( filter from filterM @(via Identity)
, mapAndUnzip from mapAndUnzipM @(via Identity)
, replicate from replicateM @(via Identity)
, zipWith from zipWithM @(via Identity)
, replicateConcurrently from replicateM @(via Concurrently)
, replicateConcurrently_ from replicateM_ @(via Concurrently)
) |
6b33e58 to
e7fdbc7
Compare
I'm not very excited about |
|
May I ask, what's the current status of this proposal? Here and there, cases pop up in my code where |
|
Personally this feels like an abuse of typeclasses. Typeclasses are specifically designed around coherence and having a canonical instance, whereas regular value-level Haskell is designed around composing and building pieces in incredibly flexible ways. This seems like trying to force typeclasses to do things they are not designed for, and I don't find it very readable or beginner friendly. Here is a blog post I wrote relating to this that I think is quite relevant to this proposal. |
|
Can you turn your blog post into a proposal tysonzero |
|
To be honest part of my proposal is just to ask the community to not overuse typeclasses, and try and build types first, and then add typeclasses when canonical/globally-coherent values of these types are needed. For example I am sad that With that said, actually doing the above is more awkward then it needs to be, so I can definitely put together a proposal to go after the current ergonomic issues: E.g. Is ergonomically nicer but less useful than: I would like the former to enable me to do everything I can do with the latter, just like the underlying core, although of course without any of the I also have some more things to consider such as how to deal with superclasses, as they make it so the structure you can get out of an instance is larger than the structure you have to put in to make the instance in the first place, assuming the superclass instances have already been defined. |
|
Apart from the community changing did you look at Coherent Explicit Dictionary Application for Haskell? You both propose a dictionary solution, I think it's the wrong way but it sounds like it solves what you want |
|
I haven't read through it particularly thoroughly but it doesn't seem overly relevant. I am not looking for coherence or global uniqueness, I want different behavior based on what parameter you pass in, which is pretty antithetical to the former (and to typeclasses in general). I just don't see the appeal of using something that is essentially a much less flexible and powerful version of passing in a parameter. Particularly when the syntax and desugaring is quite beginner unfriendly and magical. There are a variety of useful things that you can do with a parameter that will be quite problematic when trying to use You could technically do the above using type level naturals, but this will not generalize to more complex parameters. You could do the above using a parameter at the type level, but then you are in for some serious pain if you want to get that value based on information present at runtime. Not sure how you would go about using ApplyingVia in the above, as there is only one This seems like it would be pretty painful, as This is just a small example, but the general idea is that these instances are very much second class citizens. You can only do the hard coded things with them that various extensions say you can do. They aren't real values. I'm sure the above list is far from complete, value-level Haskell has a massive amount of power and flexibility. I enjoy higher order functions and algebraic structures and am very happy that they are a big part of Haskell, and all of this feels like a step in the opposite direction. I want to be able to talk about things like monoids and rings and serializers and monads as first class values. I then also want to seamlessly transition from these first class objects to and from instances, when the convenience and power of global coherence and canonicity are beneficial to me. I don't want to have to only talk about one single blessed instance per type, and then try to carefully manage a variety of extensions to coerce them from one to another. |
You can't beat values in terms of ease of use, people like Gabriel have written about this. Why not use first-class values, I will try to answer these questions in a blog post but I think the choice is not obvious |
|
Your examples are possible except the last one which doesn't have to do with the extension, Dependent Haskell will add a lot of power |
Can you show me what they would look like?
I like dependent types, but this is absolutely not where I want to use them. |
|
Just to give another perspective. I am really excited for the proposal and never ever wanted more value-level haskell via dictionary passing like @tysonzero is proposing, I just feel like it doesn't address the problems i have. I see applying-via as a great tool when a single blessed instance is not possible and we have the situation that once we have chosen the correct instance, we want to use it coherently in the function we're calling. Passing dictionaries is more flexible, but I (almost?) never want the full flexibility. Once i've committed, i only want to use the single instance. Working with type-classes makes writing abstract code so much more enjoyable. I can say: I have an abstract thing with property 1,2,3 and here's what I want to do with it. It's really a joy to write. But type-classes show their pain when the thing you've got have multiple, equally important instances. All those new types makes code really hard to read and understand. For me, applying via solves a real problem. It also might be that the other 100 times I call the function the default instance is the correct one and I don't have the problem of choosing. Which mean I don't want to refactor the function. Since I am doing some computational math with Haskell, the perfect example is the ring with two possible monoid-instances: One for addition, one for multiplication. I explicitly don't want dictionary passing, any additional flexibility can actively harm me, I still want to rely on coherency when writing abstract code. But I have two equally important instances when the thing i have is a ring. For me, a blessed canonical instances works 95% of the time, but it sometimes happens that I have to juggle a lot of newtypes. This proposal would really reduce the pain and i really hope it moves forward! |
|
I'm not proposing getting rid of typeclasses or typeclass-based functions. I'm just saying that when you want that flexibility you should just accept a parameter, and whenever you want coherence instead then use typeclasses.
|
|
@tysonzero while i may be not as clear as i wanted to be, but i read your blogpost and your posts. I might have misunderstood something. ApplyingVia is a weird hybrid where you are using a bunch of code generation to get something that feels like an incoherent instance to get custom local behavior, but that technically doesn't directly involve incoherence due to all the implicit coerces. i was trying to argue that this is in fact sometimes very useful to the, because it complements the usually typeclass-mechanism (with the ring-example). It feels (to me) like your description has a negative connotation, but it's exactly what i argue is very useful to me and why. Sometimes, the type class solution just works perfectly for 95% of use-cases and then you have a thing (like the ring) without a canonical instance and now you're in pain because of all the newtypes. This would really help me in this situation, since I won't change it to a non-typeclass based method (because it works so well for the other 95% or passing dictionaries would be quite painful to write). This really happened to me and it looks like would also benefit other (theMatten mentioned he would like to have it). |
I can't speak for @tysonzero but perhaps #324 is something like what you're looking for? For whatever little it's worth I am strongly in the camp of avoiding further incremental patching of the deriving mechanism. There's an incredible wealth of use cases for "deriving" instances that cannot be served by the baked in notion of representational type equality available in the compiler. Sometimes you want to map an instance along an isomorphism, sometimes merely along a homomorphism, and very often these morphisms are not statically known (or at least it is inconvenient to shunt enough of the logic into the type system to reify them statically). IMO the best and most beautiful features of any system are the ones that emerge spontaneously from the interaction/composition of simpler features. I think that |
|
@Icelandjack I always come back thinking about this proposal. I personally really like it. I wonder....can this be implemented as an GHC-plugin? I am not exactly sure as it's a bit over my head...but I that it's possible. |
|
I made a plugin that did this: It would turn sort @(Int `via` Down Int) [1,2,3] into coerceVia (sort @Down Int) (sort @Int) [1,2,3]However if an instance doesn't already exist, like with foldMap @_ @(Int `via` Sum Int) -> coerceVia (foldMap @_ @Int) (foldMap @_ @(Sum Int))This doesn't work, as By the way, this compiles. coerceVia @(Monoid Int) (foldMap @_ @Int) (foldMap @_ @(Sum Int))Any ideas for where to go next? |
Applying Via
This proposes a new language extension
ApplyingViato change the behaviour of types.TypeApplicationsallows applying terms to an "at type"; applying via allows specifying a via type which is representationally equal to the at type. The new behaviour is inherited from instances of the via type.This will allow
sortto sort "down"We discard the term-level Down and only use its type-level information just as
ala. Applying via@(via f)an argumentf :: proxy <at> <via>(usuallyproxy ~ (->)) means we get behaviour from the<via>type but end up at the<at>type. A more explicit syntax;@(<at> via <via>).Downinsort @(via Down)is a term-level proxy of typeDown :: a -> Down aand has the same meaning assort @(forall a. a via Down a)(haven't figured the quantification out).for_loops which are usually left-to-right can iterate viaReverse, right-to-leftThese use the same
IOeffect with sequential behaviour. For concurrent behaviour we can apply viaConcurrently:This allows defining standard combinators:
Rather than
we define