Send Beginners mailing list submissions to
beginners@haskell.org
To subscribe or unsubscribe via the World Wide Web, visit
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
beginners-requ...@haskell.org
You can reach the person managing the list at
beginners-ow...@haskell.org
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Trying to prove Applicative is superclass of Functor,
etc (Silent Leaf)
2. Re: Trying to prove Applicative is superclass of Functor,
etc (Silent Leaf)
3. Re: Trying to prove Applicative is superclass of Functor,
etc (Daniel Bergey)
4. Re: Trying to prove Applicative is superclass of Functor,
etc (D?niel Arat?)
----------------------------------------------------------------------
Message: 1
Date: Fri, 29 Apr 2016 14:43:08 +0200
From: Silent Leaf <silent.le...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Trying to prove Applicative is
superclass of Functor, etc
Message-ID:
<cagfccjpn6xqkbcpgqvccetuebydosorfzbweenn-n2oerdk...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
I didn't get this version of ghc already existed! it seems I have it, i'll
thus check all that ASAP.
Technical question: class constraints should not be written in definitions
of instances too, right? Wouldn't be "parametric" anymore and all:
> instance Applicative Maybe => Monad Maybe where ...
I don't think I've ever seen something like that but I'm asking just in
case, esp as it might precisely be the way to write implied superclasses in
the latest ghc(?)
Indeed, your definition of (<*>) in terms of monads is much simpler to
read! I think I was too much centered on finding a way to replicate the
types, to more simply find a way to replicate directly what does the
function.
Obviously, my def can become yours by some simple operations.
Mine:
> let left = mf >>= \f -> return $ return . f
> right = \mg -> ma >>= mg
> in left >>= right
Here with mg = return . f eventually (when called).
Two things bound together, the wrapped value of left (== return.f) being
the parameter of the function right. It's clear that the wrapped result is
just wrapped so it can be unwrapped immediately after. Might as well not
wrap it at all in the first place, and do everything in the first bind
operation:
> mf >>= \f -> let mg = return . f in ma >>= mg
and of course, (mg == \a -> return $ f a).
Anyway, yeah that's also how I read (=>) arrows, obviously, how else to do?
^^ It's just, as most of the syntax and terminology of haskell is based on
what looks like very solid math roots, I imagined the syntax for
constraints was also justified mathematically somehow.
Le vendredi 29 avril 2016, D?niel Arat? <exitcons...@gmail.com> a ?crit :
> For a drunk person you're getting these equivalences surprisingly right.
:)
>
>>> Ah true, I heard about this D?niel. But then it would be generalized to
>> all classes, or just those three ones?
>
> It would make sense for it to work for any class hierarchy, but
> honestly I just don't know and I've got an old GHC on my laptop so I
> can't check. Maybe someone who actually knows will come along and
> enlighten us. ?\_(?)_/?
>
>>> Anyway, trying the same with Applicative and its *sub*class Monad:
>>>> pure = return
>
> That's right.
>
>>>> mf <*> ma =
>>> let mg = mf >>= \f -> return (return . f)
>>> in mg >>= \g -> (ma >>= g)
>
>>> Is there an easier solution? It's easy enough, but not as trivial as for
>> Applicative => Functor.
>
> I've got (an alpha-equivalent of) the following on a scrap piece of paper:
> mf <*> mx = mf >>= \f -> mx >>= \x -> return . f $ x
>
> It reads nice and fluent.
>
>>> Why do we write constraints like that:
>>>> Functor f => (a -> b) -> f a -> f b
>>> or:
>>>> Functor f => Applicative f
>
> That's a very good question. I agree that it would make a bit more
> sense if the arrows were reversed.
> I think it helps to read
> "Functor f => Applicative f where ..."
> as
> "if you've got a Functor then you can have an Applicative if you just
> implement these functions"
> as opposed to
> "if f is a Functor that implies that f is an Applicative" (wrong).
>
> Daniel
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20160429/29f204ef/attachment-0001.html>
------------------------------
Message: 2
Date: Fri, 29 Apr 2016 14:54:02 +0200
From: Silent Leaf <silent.le...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Trying to prove Applicative is
superclass of Functor, etc
Message-ID:
<CAGFccjMBBVBUSg8OSwmjisLFpKOS70HEL4ZpxpokKJDG=iv...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Well, I think it didn't work. From:
> data Foo a = Foo a
> instance Monad Foo where
> return = Foo
> (Foo a) >>= f = f a
I got:
No instance for (Applicative Foo)
arising from the superclasses of an instance declaration
In the instance declaration for ?Monad Foo?
Doesn't seem to build 'em automatically. :(
Le vendredi 29 avril 2016, Silent Leaf <silent.le...@gmail.com> a ?crit :
> I didn't get this version of ghc already existed! it seems I have it,
i'll thus check all that ASAP.
> Technical question: class constraints should not be written in
definitions of instances too, right? Wouldn't be "parametric" anymore and
all:
>> instance Applicative Maybe => Monad Maybe where ...
> I don't think I've ever seen something like that but I'm asking just in
case, esp as it might precisely be the way to write implied superclasses in
the latest ghc(?)
>
> Indeed, your definition of (<*>) in terms of monads is much simpler to
read! I think I was too much centered on finding a way to replicate the
types, to more simply find a way to replicate directly what does the
function.
> Obviously, my def can become yours by some simple operations.
> Mine:
>> let left = mf >>= \f -> return $ return . f
>> right = \mg -> ma >>= mg
>> in left >>= right
> Here with mg = return . f eventually (when called).
>
> Two things bound together, the wrapped value of left (== return.f) being
the parameter of the function right. It's clear that the wrapped result is
just wrapped so it can be unwrapped immediately after. Might as well not
wrap it at all in the first place, and do everything in the first bind
operation:
>> mf >>= \f -> let mg = return . f in ma >>= mg
> and of course, (mg == \a -> return $ f a).
>
> Anyway, yeah that's also how I read (=>) arrows, obviously, how else to
do? ^^ It's just, as most of the syntax and terminology of haskell is based
on what looks like very solid math roots, I imagined the syntax for
constraints was also justified mathematically somehow.
>
> Le vendredi 29 avril 2016, D?niel Arat? <exitcons...@gmail.com> a ?crit :
>> For a drunk person you're getting these equivalences surprisingly right.
:)
>>
>>>> Ah true, I heard about this D?niel. But then it would be generalized to
>>> all classes, or just those three ones?
>>
>> It would make sense for it to work for any class hierarchy, but
>> honestly I just don't know and I've got an old GHC on my laptop so I
>> can't check. Maybe someone who actually knows will come along and
>> enlighten us. ?\_(?)_/?
>>
>>>> Anyway, trying the same with Applicative and its *sub*class Monad:
>>>>> pure = return
>>
>> That's right.
>>
>>>>> mf <*> ma =
>>>> let mg = mf >>= \f -> return (return . f)
>>>> in mg >>= \g -> (ma >>= g)
>>
>>>> Is there an easier solution? It's easy enough, but not as trivial as
for
>>> Applicative => Functor.
>>
>> I've got (an alpha-equivalent of) the following on a scrap piece of
paper:
>> mf <*> mx = mf >>= \f -> mx >>= \x -> return . f $ x
>>
>> It reads nice and fluent.
>>
>>>> Why do we write constraints like that:
>>>>> Functor f => (a -> b) -> f a -> f b
>>>> or:
>>>>> Functor f => Applicative f
>>
>> That's a very good question. I agree that it would make a bit more
>> sense if the arrows were reversed.
>> I think it helps to read
>> "Functor f => Applicative f where ..."
>> as
>> "if you've got a Functor then you can have an Applicative if you just
>> implement these functions"
>> as opposed to
>> "if f is a Functor that implies that f is an Applicative" (wrong).
>>
>> Daniel
>> _______________________________________________
>> Beginners mailing list
>> Beginners@haskell.org
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20160429/59f45ec8/attachment-0001.html>
------------------------------
Message: 3
Date: Fri, 29 Apr 2016 09:03:20 -0400
From: Daniel Bergey <ber...@alum.mit.edu>
To: Silent Leaf <silent.le...@gmail.com>, The Haskell-Beginners
Mailing List - Discussion of primarily beginner-level topics related
to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Trying to prove Applicative is
superclass of Functor, etc
Message-ID:
<87inz0sh2f.fsf@chladni.i-did-not-set--mail-host-address--so-tickle-me>
Content-Type: text/plain
My understanding is that both the -> and => arrows represent
implication, in the Curry-Howard view of types as proofs. Maybe someone
else can provide better examples of translating back and forth this way.
I'd interpret fmap in English as something like:
`fmap g fa` is a proof that for all f, g, fa, given that f is a Functor
and given g is a function from a to b, and given fa has type `f a`,
there is a value of type `f b`.
You can shuffle things around in other ways, like:
... for all f, g, ... there is a function from `f a` to `f b`.
The => in instance definitions plays a similar role:
Num a => Num (V2 a) where ...
means: For all types a, given that a is a Num, it follows that `V2 a` is
a Num (as proven by the following definitions ...)
A class definition with a superclass requirement means something like:
Functor f => Applicative f where ...
You can show that a type f is an Applicative by providing a proof (type
class instance) that f is a Functor, and proofs (definitions) of the
following class functions.
I hope this helps, and that I've gotten it right.
bergey
On 2016-04-29 at 06:16, Silent Leaf <silent.le...@gmail.com> wrote:
> Which leads me to one question I have for a long now. I haven't found my
> answer, but perhaps did I not search at the right place...
>
> Why do we write constraints like that:
>> Functor f => (a -> b) -> f a -> f b
> or:
>> Functor f => Applicative f
> I'm far from an expert in Math, but I'm used to reading (=>) as an
> implication, but maybe is it completely different? At any rate, if
> it were an implication, i'd expect it to be written for example (Applicative
> f => Functor f), to denote maybe that anything being an
> Applicative should also be a functor (everything in the first is (= must be,
> in declarative terms) in the second). I mean if we see a
> class as a set of types (can we btw?) then if A(pplicative) is superclass of
> M(onad), A is a superset of M, because (m in M) => (m in
> A), hence the direction of the implication arrow, Monad => Applicative.
>
> Same thing for types of function (and other values), eg (a -> b => Num a),
> the type of the function would imply some constraint, which
> would therefore imply that no type that doesn't respect the implied term
> (constraint) can pretend to be "part" of the type of the
> function/value.
>
> Maybe I'm misinterpreting the purpose or meaning, but I still wonder what is
> the actual meaning then of those (=>) arrows as they
> don't *seem* to be implications in the mathematical meaning I'd intuitively
> imagine.
------------------------------
Message: 4
Date: Fri, 29 Apr 2016 17:44:44 +0200
From: D?niel Arat? <exitcons...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Trying to prove Applicative is
superclass of Functor, etc
Message-ID:
<cahvkd2lb6ehtlpg+gtrsdhwfw_lhxci6uqebzrpzn0j+q+w...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
Excellent answer. I kind of suspected the same but I couldn't quite
find an appropriate translation for "=>".
It's not really implication though. At least not in the same sense as "->". :(
On 29/04/2016, Daniel Bergey <ber...@alum.mit.edu> wrote:
> My understanding is that both the -> and => arrows represent
> implication, in the Curry-Howard view of types as proofs. Maybe someone
> else can provide better examples of translating back and forth this way.
(snip)
> A class definition with a superclass requirement means something like:
>
> Functor f => Applicative f where ...
>
> You can show that a type f is an Applicative by providing a proof (type
> class instance) that f is a Functor, and proofs (definitions) of the
> following class functions.
>
> I hope this helps, and that I've gotten it right.
>
> bergey
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 94, Issue 31
*****************************************
