[Haskell-cafe] Strange things with type literals of kind Nat

[Troels Henriksen]

Consider the following definition of lists with a statically determined
minimum length.

data Nat' = Z | S Nat'

data NList (n::Nat') a where
  Rest :: [a] -> NList Z a
  (:>) :: a -> NList n a -> NList (S n) a

uncons :: NList (S n) a -> (a, NList n a)
uncons (x :> xs) = (x, xs)

This works fine.  Now consider an implementation using the new type
literals in GHC:

data NList (n::Nat) a where
  Rest :: NList 0 [a]
  (:>) :: a -> NList n a -> NList (n+1) a

uncons :: NList (n+1) a -> NList n a
uncons (x :> l) = l

This gives a type error:

/home/athas/code/nonempty_lists.hs:41:19:
Could not deduce (n1 ~ n)
from the context ((n + 1) ~ (n1 + 1))
  bound by a pattern with constructor
 :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,
   in an equation for `uncons'
  at /home/athas/code/nonempty_lists.hs:41:9-14
  `n1' is a rigid type variable bound by
   a pattern with constructor
 :> :: forall a (n :: Nat). a -> NList n a -> NList (n + 1) a,
   in an equation for `uncons'
   at /home/athas/code/nonempty_lists.hs:41:9
  `n' is a rigid type variable bound by
  the type signature for uncons :: NList (n + 1) a -> NList n a
  at /home/athas/code/nonempty_lists.hs:40:11
Expected type: NList n a
  Actual type: NList n1 a
In the expression: l
In an equation for `uncons': uncons (x :> l) = l

I don't understand why GHC cannot infer that the two types are the same.
My guess is that 'n+1' is not "structural" to GHC in the same way that
'S n' is.  The page
http://hackage.haskell.org/trac/ghc/wiki/TypeNats/MatchingOnNats
mentions that "type level numbers of kind Nat have no structure", which
seems to support my suspicion.  What's the complete story, though?

-- 
\  Troels
/\ Henriksen

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Associative prefix operators in Parsec

[Troels Henriksen]

Christian Maeder  writes:

> The simplest solution is to parse the prefixes yourself and do not put
> it into the table.
>
> (Doing the infixes "&" and "|" by hand is no big deal, too, and
> possibly easier then figuring out the capabilities of
> buildExpressionParser)

Is there another solution?  My post was a simplified example to showcase
the problem; in general I would prefer to use a function to build the
expression parser.  I could just write my own that does not have this
problem, and in fact, I already have, I just wanted to know whether
Parsec could be wrangled into shape.

-- 
\  Troels
/\ Henriksen

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Associative prefix operators in Parsec

[Troels Henriksen]

Consider a simple language of logical expressions:

> import Control.Applicative
> import Text.Parsec hiding ((<|>), many)
> import Text.Parsec.String
> import Text.Parsec.Expr
>
> data Expr = Truth
>   | Falsity
>   | And Expr Expr
>   | Or Expr Expr
>   | Not Expr
> deriving (Show, Eq)

I define a simple expression parser using Parsec:

> expr :: Parser Expr
> expr= buildExpressionParser table (lexeme term)
>  "expression"
> 
> term :: Parser Expr
> term=  between (lexeme (char '(')) (lexeme (char ')')) expr
> <|> bool
>  "simple expression"
> 
> bool :: Parser Expr
> bool = lexeme (string "true" *> pure Truth)
><|> lexeme (string "false" *> pure Falsity)
> 
> lexeme :: Parser a -> Parser a
> lexeme p = p <* spaces
> 
> table   = [ [prefix "!" Not ]
>   , [binary "&" And AssocLeft ]
>   , [binary "|" Or AssocLeft ]
>   ]
> 
> binary  name fun assoc = Infix (do{ lexeme (string name); return fun }) assoc
> prefix  name fun   = Prefix (do{ lexeme (string name); return fun })

Now this doesn't work:

> test1 = parseTest expr "!!true"

But this does:

> test2 = parseTest expr "!(!true)"

I have studied the code for buildExpressionParser, and I know why this
happens (prefix operators are treated as nonassociative), but it seems
like one would often want right-associative prefix operators (so test1
would work).  Is there a common workaround or solution for this problem?
I assume the nonassociativity in Parsec is by design and not a bug.

-- 
\  Troels
/\ Henriksen

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe