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. Programming with Singletons (Quentin Liu)
2. Re: Programming with Singletons (mukesh tiwari)
3. Re: Relation between Effects, Indexed monads, Free monads
(PY) (鲍凯文)
----------------------------------------------------------------------
Message: 1
Date: Wed, 15 Nov 2017 19:21:57 -0500
From: Quentin Liu <quentin.liu.0...@gmail.com>
To: beginners@haskell.org
Subject: [Haskell-beginners] Programming with Singletons
Message-ID: <bd3803da-8440-4c02-9f03-8d0bbf7b198d@Spark>
Content-Type: text/plain; charset="utf-8"
Hi all,
I was doing the “Singletons” problem at codewars[1]. The basic idea is to use
dependent types to encode the length of the vector in types.
It uses
data Nat = Zero | Succ Nat
data SNat a where
SZero :: SNat Zero
SSucc :: SNat a -> SNat (Succ a)
to do the encoding.
The vector is defined based on the natural number encoding:
data Vec a n where
VNil :: Vec a Zero
VCons :: a -> Vec a n -> Vec a (Succ n)
There are some type families declared for manipulating the natural numbers, and
one of them that is relevant to the question is
type family (Add (a :: Nat) (b :: Nat)) :: Nat
type instance Add Zero b = b
type instance Add a Zero = a
type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))
where the `Add` function adds natural numbers.
The problem I am stuck with is the concatenation of two vectors:
(++) :: Vec v m -> Vec v n -> Vec v (Add m n)
VNil ++ b = b
(VCons x xs) ++ b = VCons x $ xs ++ b
The program would not compile because the compiler found that `VCons x $ xs ++
b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the declared type
`Vec v (Add m n)`. Is it because ghc does not expand `Add m n’ that the type
does not match? I read Brent Yorgey’s blog on type-level programming[2] and he
mentioned that would not automatically expand types. But the posted time of the
blog is 2010 and I am wondering if there is any improvement to the situation
since then? Besides, what would be the solution to this problem
Warm Regards,
Qingbo Liu
[1] https://www.codewars.com/kata/singletons/train/haskell
[2]
https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20171115/06cbb447/attachment-0001.html>
------------------------------
Message: 2
Date: Thu, 16 Nov 2017 11:50:31 +1100
From: mukesh tiwari <mukeshtiwari.ii...@gmail.com>
To: The Haskell-Beginners Mailing List - Discussion of primarily
beginner-level topics related to Haskell <beginners@haskell.org>
Subject: Re: [Haskell-beginners] Programming with Singletons
Message-ID:
<cafhzve-aefy+vdueucnnrv2vg0y1usb2kpkitt41_adbrwn...@mail.gmail.com>
Content-Type: text/plain; charset="UTF-8"
Hi Quentin,
I changed your pattern little bit in Add function and it is working
fine. I think the problem was that type of (VCons x xs) ++++ b is Vec
v (Add (Succ m1) + n) which was not present in your
Add function pattern.
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE InstanceSigs #-}
module Tmp where
data Nat = Zero | Succ Nat
data SNat a where
SZero :: SNat Zero
SSucc :: SNat a -> SNat (Succ a)
data Vec a n where
VNil :: Vec a Zero
VCons :: a -> Vec a n -> Vec a (Succ n)
type family (Add (a :: Nat) (b :: Nat)) :: Nat
type instance Add Zero b = b
type instance Add (Succ a) b = Succ (Add a b)
(++++) :: Vec v m -> Vec v n -> Vec v (Add m n)
VNil ++++ b = b
(VCons x xs) ++++ b = VCons x $ xs ++++ b
On Thu, Nov 16, 2017 at 11:21 AM, Quentin Liu
<quentin.liu.0...@gmail.com> wrote:
> Hi all,
>
> I was doing the “Singletons” problem at codewars[1]. The basic idea is to
> use dependent types to encode the length of the vector in types.
>
> It uses
> data Nat = Zero | Succ Nat
>
> data SNat a where
> SZero :: SNat Zero
> SSucc :: SNat a -> SNat (Succ a)
> to do the encoding.
>
> The vector is defined based on the natural number encoding:
> data Vec a n where
> VNil :: Vec a Zero
> VCons :: a -> Vec a n -> Vec a (Succ n)
>
>
> There are some type families declared for manipulating the natural numbers,
> and one of them that is relevant to the question is
> type family (Add (a :: Nat) (b :: Nat)) :: Nat
> type instance Add Zero b = b
> type instance Add a Zero = a
> type instance Add (Succ a) (Succ b) = Succ (Succ (Add a b))
> where the `Add` function adds natural numbers.
>
> The problem I am stuck with is the concatenation of two vectors:
> (++) :: Vec v m -> Vec v n -> Vec v (Add m n)
> VNil ++ b = b
> (VCons x xs) ++ b = VCons x $ xs ++ b
>
> The program would not compile because the compiler found that `VCons x $ xs
> ++ b`gives type `Vec v (Succ (Add n1 n))`, which does not follow the
> declared type `Vec v (Add m n)`. Is it because ghc does not expand `Add m n’
> that the type does not match? I read Brent Yorgey’s blog on type-level
> programming[2] and he mentioned that would not automatically expand types.
> But the posted time of the blog is 2010 and I am wondering if there is any
> improvement to the situation since then? Besides, what would be the solution
> to this problem
>
>
> Warm Regards,
> Qingbo Liu
>
> [1] https://www.codewars.com/kata/singletons/train/haskell
> [2]
> https://byorgey.wordpress.com/2010/07/06/typed-type-level-programming-in-haskell-part-ii-type-families/
>
>
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
------------------------------
Message: 3
Date: Wed, 15 Nov 2017 18:29:08 -0800
From: 鲍凯文 <traqueofzi...@gmail.com>
To: beginners@haskell.org
Subject: Re: [Haskell-beginners] Relation between Effects, Indexed
monads, Free monads (PY)
Message-ID:
<CAMjcG+GxtyOKCMkCzx=sqdbk-q1jgye1ksdc2p+pqjsogfp...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
Hi,
Disclaimer: I am not a lawyer. Nor do I claim to understand all this stuff.
The enforcement of sequential ordering is sort of baked into monads; the
haskell (read: do-notation) way of combining monadic computations is using
bind (i.e. in the "fancy list of instructions with a way to bind results").
This is only for the structure of the computation, though. Every monadic
computation is still a pure function, so in the end the RTS, well, executes
parts of those at a time, just as pure functions.
The ordering guarantee that more corresponds to imperative programming is
most obvious (to me) with ST, IO, and State; data dependencies ensure that
things "later" in the monadic chain cannot be executed until everything
"before". But those effects all involve (mutable) state. Monadic chaining,
i.e. combining effectful computations, is separate from the concept of
mutable state, etc. It seems more like just an algebra for effects.
If you're talking about marked monads as in those with extra type
information or phantom params, like when used in tandem with the rank-2
type trick (used in ST, region-based IO, etc.), I think that's a little
different, or at least beyond what monads are. Those were created to handle
things like guaranteeing that state is only modified single-threadedly
(ST), or to ensure that you can't do things like forget to close a handle
or leak a ref to a closed one (regions).
I think Free monads and (Kiselyov's) Eff monad are still different. They
still appeal to the "monads as sequence of instructions" view, but uh,
especially with the Eff monad, they're pretty fancy. As in at least
personally, for "normal" programming, I haven't felt the need to delve into
them.
I think the important upshot is: what are you working on? Do monadic
computations model what you want to do naturally? If they do, do you need
something stronger than what they provide? It's hard to answer the latter
questions without answering the first.
Sorry for rambling,
toz
On Wed, Nov 15, 2017 at 4:00 AM, <beginners-requ...@haskell.org> wrote:
> 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. Relation between Effects, Indexed monads, Free monads (PY)
>
>
> ----------------------------------------------------------------------
>
> Message: 1
> Date: Wed, 15 Nov 2017 14:15:13 +0200
> From: PY <aqua...@gmail.com>
> To: beginners@haskell.org
> Subject: [Haskell-beginners] Relation between Effects, Indexed monads,
> Free monads
> Message-ID: <f34c805e-bad4-845e-d09b-43d9a9bae...@gmail.com>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> Hello, All!
>
> I'm not sure is it question for Cafe or Beginners List, so first I'll
> try here.
>
> There are kind of errors related to wrong execution sequence. They are
> good known in OOP: object keeps state internally and check it before to
> execute got message - to prevent wrong execution sequence. Best
> implementation is: state machine, also can be used Markov's algorithm,
> more complex can be done with Petri nets, etc.
>
> Example: if I have complex inserting into DB (consisting of several
> inserts), I can check done of previous step before to start next, etc.
> After read of different Haskell resources I found solution for it:
> Indexed Monads. They (if I got it rightly) are monads with additional
> type parameter which "marks" monad, gives it more specific
> qualification, for example instead of monad "Opening" (action) we have
> monad "Opening-of-closed", exactly what I'm talking: type-level check of
> correct actions sequence (allowed transition).
>
> After more research I found Free Monads and Effects and something like
> "free monad can be used to proof your program". How?! Free monads make
> "active" (executable) code into "passive" code (data instead of code),
> which can be interpreted separately, so program becomes like Lisp
> program: code is a data (so, can be modified, checked, etc, etc) and
> what exactly will be executing - decides interpreter of such code. But
> do they allow to proof right sequence of actions in such data-like code?
>
> What are the Effects I don't understand yet.
>
> Somewhere I find something like: Eff = Free Monad + indexed monad (may
> be I'm not right here). So my questions are:
>
> - how Effects, Free Monad, Indexed Monads are related?
>
> - can effects replace indexed monads?
>
> - are indexed monad yet usable/modern concept or they are abandoned and
> replaced by Effects or something else? Do you use indexed monads in real
> projects?
>
> - can I (and how) to use both of them? Or: can I use only FreeMonads /
> Effects to solve the same problem (control of correct sequence of
> actions) like with indexed monads help?
>
>
> ===
>
> Best regards, Paul
>
>
>
> ------------------------------
>
> Subject: Digest Footer
>
> _______________________________________________
> Beginners mailing list
> Beginners@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
>
>
> ------------------------------
>
> End of Beginners Digest, Vol 113, Issue 10
> ******************************************
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20171115/06bae7ea/attachment.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 113, Issue 12
******************************************
