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. lookAhead (Dennis Raddle)
2. Re: Multiplicaton of singletons (Dmitriy Matrosov)
----------------------------------------------------------------------
Message: 1
Date: Tue, 15 Mar 2016 19:17:58 -0700
From: Dennis Raddle <dennis.rad...@gmail.com>
To: Haskell Beginners <beginners@haskell.org>
Subject: [Haskell-beginners] lookAhead
Message-ID:
<CAKxLvoqJY13ZY18KFpxkXY=7o8BEB8-++M=hyjiabulg0s-...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
I'm working with "lookAhead" in Parsec.
My goal is to simplify error messages and make them more relevant. I'm
parsing strings that represent musical score text markings that convey
nuances of playback expression. I worked long and hard to devise a concise
syntax that has sufficient expressive power --- must be concise because
there is little room in these score for text markings, especially if there
are a lot of them. The result is that it looks a little cryptic.
1;%2|>
<%4|
<<5:4
<<5:4a
etc.
My first parser worked, but would give error messages like
"Unexpected ';', expected digit, ';', '%', '<<', '|', ....
etc., basically giving me no clue what the parser was thinking.
The first challenge is that it's hard to identify the particular type of
mark from the first few characters. For instance, a mark like this "1;%2|>"
--- what gives it away is the ">" at the very end. That means it's a
"right-facing warp" and that defines what to expect in the other
characters. So it would be great if my parser first identified this as a
"right-facing warp" and then when parsing the internals it can give
messages that make sense in context.
So I tried this, with lookAhead
rightWarp = do
try (lookAhead (do many1 (noneOf "<>")
char '>'
eof))
... parse internals ...
char '>'
eof
The problem is that I want to put a <?> message in here somewhere so that
if this whole 'rightWarp' parser fails, it will say "expected right warp".
But I have found with experiment that the parser considers the point of
failure to be in different places inside the lookAhead. For instance if I
give an input string that has too many characters at the end, the failure
point will be the 'eof' inside the lookAhead. If I put a <?> message
anywhere else, the parser will just say "expected end of input". On the
other hand, if there is no '>' character, then the failure point will be
"char '>'" and the message will be "expected >".
What I was hoping was that there was some single place I could put a <?>
message that would say "expected right warp" no matter where inside
rightWarp the failure point occurs.
Any ideas?
Mike
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20160315/2af3989a/attachment-0001.html>
------------------------------
Message: 2
Date: Wed, 16 Mar 2016 13:08:44 +0300
From: Dmitriy Matrosov <sgf....@gmail.com>
To: beginners@haskell.org
Subject: Re: [Haskell-beginners] Multiplicaton of singletons
Message-ID:
<cafdvufmkn0xt1epefwba3oazic48j2z31rm6emvjxhkxr6x...@mail.gmail.com>
Content-Type: text/plain; charset="utf-8"
On Tue, Mar 15, 2016 at 1:23 PM, Dmitriy Matrosov <sgf....@gmail.com> wrote:
> > {-# LANGUAGE DataKinds, KindSignatures, TypeFamilies,
> UndecidableInstances #-}
>
> Hi.
>
> I've reading "Part I: Dependent Types in Haskell" by Hiromi ISHII at
> schoolofhaskell [1] and i can't understand why my multiplication for
> singletons (that was exercise) does not not work:
>
> > data Nat = Z | S Nat
> >
> > type family Plus (a :: Nat) (b :: Nat) :: Nat where
> > Plus 'Z b = b
> > Plus ('S a1) b = 'S (Plus a1 b)
> >
> > type family Mult (a :: Nat) (b :: Nat) :: Nat where
> > Mult 'Z b = 'Z
> > Mult ('S 'Z) b = b
> > Mult ('S a1) b = Plus (Mult a1 b) b
> >
> > data SNat :: Nat -> * where
> > SZ :: SNat 'Z
> > SN :: SNat n -> SNat ('S n)
> >
> > plusN :: SNat n -> SNat m -> SNat (Plus n m)
> > plusN SZ y = y
> > plusN (SN x) y = SN (plusN x y)
> >
> > multN :: SNat n -> SNat m -> SNat (Mult n m)
> > multN SZ y = SZ
> > multN (SN SZ) y = y
> > multN (SN x) y = plusN (multN x y) y
>
> The last line (multN) does not type-check with error:
>
> 1.lhs:31:25:
> Could not deduce (Mult ('S n1) m ~ Plus (Mult n1 m) m)
> from the context (n ~ 'S n1)
> bound by a pattern with constructor
> SN :: forall (n :: Nat). SNat n -> SNat ('S n),
> in an equation for ?multN?
> at 1.lhs:31:10-13
> Expected type: SNat (Mult n m)
> Actual type: SNat (Plus (Mult n1 m) m)
> Relevant bindings include
> y :: SNat m (bound at 1.lhs:31:17)
> x :: SNat n1 (bound at 1.lhs:31:13)
> multN :: SNat n -> SNat m -> SNat (Mult n m) (bound at 1.lhs:29:3)
> In the expression: plusN (multN x y) y
> In an equation for ?multN?: multN (SN x) y = plusN (multN x y) y
>
> Though, when (n ~ 'S n1) i get `SNat (Mult ('S n1) m)` and by definition of
> Mult this is `SNat (Plus (Mult n1 m) m)` . On the other hand, when i check
> the
> type of expression, i get `SNat (Plus (Mult n1 m) m)` by definition of
> plusN.
> I.e. exactly the same type.
>
>
> [1]:
> https://www.schoolofhaskell.com/user/konn/prove-your-haskell-for-great-safety/dependent-types-in-haskell
>
>
Aah, it seems, the reason is wrong (my) definition of Mult: 2nd and 3rd
type family branches are not compatible: `Mult ('S 'Z) b` and `Mult ('S a1)
b` are not apart (hm.. probably; not sure what "arbitrary type-family
simplifications" means in [2], 6.2.1) and their RHS-es are not the same
"under the substitution induced by the unification" ([2], 6.2.1). And
because 2nd branch is not needed at all, all works fine with such Mult:
> type family Mult (a :: Nat) (b :: Nat) :: Nat where
> Mult 'Z b = 'Z
> Mult ('S a1) b = Plus (Mult a1 b) b
[2]: https://wiki.haskell.org/GHC/Type_families#Closed_family_simplification
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://mail.haskell.org/pipermail/beginners/attachments/20160316/b2494173/attachment-0001.html>
------------------------------
Subject: Digest Footer
_______________________________________________
Beginners mailing list
Beginners@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/beginners
------------------------------
End of Beginners Digest, Vol 93, Issue 11
*****************************************
