Re: [Haskell-cafe] Re: Typed Lambda-Expressions withOUT GADTs
Hi,
So far, we've seen GADTs encodings based on
the ideo of turning each (value) pattern clause
into an (type class) instance declaration.
There's also another encoding based on the idea
of providing (value) evidence for type equality.
(Explored by example by quite a few people,
see upcoming paper for references).
A formal result can be found here:
A Systematic Translation of Guarded Recursive Data Types to
Existential Types
by Martin Sulzmann and Meng Wang
http://www.comp.nus.edu.sg/~sulzmann/
Example encodings for some of the
examples we've seen so far can be found below.
Martin
- Examples encodings ---
{-# OPTIONS -fglasgow-exts #-}
data E a b = E (a->b,b->a)
{-
data Sym env r
= forall xx.(env = (r,xx)) => FirstSym
| forall env' a.(env=(a,env')) => NextSym (Sym env' r)
-}
data Sym env r
= forall xx. FirstSym (E env (r,xx))
| forall env' a. NextSym (Sym env' r) (E env (a,env'))
{-
runSym :: Sym env r -> env -> r
runSym FirstSym (r,xx) = r
runSym (NextSym var) (a,env) = runSym var env
-}
-- have to play the pair trick because pattern doesn't match
runSym :: Sym env r -> env -> r
runSym (FirstSym (E (g,h))) pair {-(r,xx)-} = (fst (g pair))
runSym (NextSym var (E (g,h))) pair {-(a,env)-} = runSym var (snd (g
pair))
{-
data OpenExpression env r
= forall a r'.(r=(a->r')) => Lambda (OpenExpression (a',env) r')
| forall r'. Symbol (Sym env r)
| Constant r
| forall a. Lambda (OpenExpression env (a -> r))
(OpenExpression env a)
-}
data OpenExpression env r
= forall a r'. Lambda (OpenExpression (a,env) r') (E r (a->r'))
| Symbol (Sym env r)
| Constant r
| forall a. Application (OpenExpression env (a -> r))
(OpenExpression env a)
{-
runOpenExpression :: OpenExpression env a -> env -> a
runOpenExpression (Constant r) _ = r
runOpenExpression (Application ar a) env = (runOpenExpression ar env)
(runOpenExpression a env)
runOpenExpression (Lambda exp) env = \a -> runOpenExpression exp
(a,env)
runOpenExpression (Symbol var) env = runSym var env
-}
runOpenExpression :: OpenExpression env a -> env -> a
runOpenExpression (Constant r) _ = r
runOpenExpression (Application ar a) env = (runOpenExpression ar env)
(runOpenExpression a env)
runOpenExpression (Lambda exp (E (g,h))) env = h (\a ->
runOpenExpression exp (a,env))
runOpenExpression (Symbol var) env = runSym var env
newtype Expression r = MkExpression (forall env. OpenExpression env r)
runExpression :: Expression r -> r
runExpression (MkExpression expr) = runOpenExpression expr ()
eid = E (id,id)
sym0 :: OpenExpression (a,env) a
sym0 = Symbol (FirstSym eid)
sym1 :: OpenExpression (a,(b,env)) b
sym1 = Symbol (NextSym (FirstSym eid) eid)
sym2 :: OpenExpression (a,(b,(c,env))) c
sym2 = Symbol (NextSym (NextSym (FirstSym eid) eid) eid)
k :: Expression (a -> b -> a)
-- k = \x.\y -> x = \.\.1
k = MkExpression (Lambda (Lambda sym1 eid) eid)
s :: Expression ((a -> b -> c) -> (a -> b) -> a -> c)
-- s = \x.\y.\z -> x z (y z) = \.\.\.2 0 (1 0)
s = MkExpression (Lambda (Lambda (Lambda (Application (Application
sym2 sym0) (Application sym1 sym0)) eid) eid) eid)
test3 = (runExpression s) (runExpression k) (runExpression k)
{-# OPTIONS
-fglasgow-exts #-}
import Control.Monad.State (MonadState (..))
data E a b = E (a->b,b->a)
data State s a
= forall b. Bind (State s a) (a -> State s b) (E a b)
| Return a
| Get (E a s)
| Put s (E a ())
runState :: State s a -> s -> (s,a)
runState (Return a) s = (s,a)
runState (Get (E (g,h))) s = (s,(h s))
runState (Put s (E (g,h))) _ = (s,(h ()))
runState (Bind (Return a) k (E (g,h))) s
= let --cast :: State s b -> State s a
cast (Return a) = Return (h a)
cast (Get (E (g',h'))) = Get (E (\x-> g' (g x),\x->h (h' x)))
cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
in runState (cast (k a)) s
runState (Bind (Get (E (g1,h1))) k (E (g,h))) s
= let cast (Return a) = Return (h a)
cast (Get (E (g',h'))) = Get (E (\x-> g' (g x),\x->h (h' x)))
cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
in runState (cast (k (h1 s))) s
runState (Bind (Put s (E (g1,h1))) k (E (g,h))) _
= let cast (Return a) = Return (h a)
cast (Get (E (g',h'))) = Get (E (\x-> g' (g x),\x->h (h' x)))
cast (Put s (E (g',h'))) = Put s (E (\x->g' (g x),\x->h (h'
x)))
cast (Bind s' k' (E (g',h'))) = Bind (cast s') (\x->k' (g x))
(E (\x->g' (g x),\x->h (h' x)))
in runState (cast (k (h1 ( s
runState (Bind (Bind m k1 (E (g1,h1))) k2 (E (g,h))) s
= runState m (\x -> Bind (k1 x) k2 (E (g,h))) s
{-
instance Monad (State s) where
(>>=) = Bind
return = Return
in
[Haskell-cafe] Two fun things with GADTs
1. Reifying class instances
Easy to do, and useful sometimes:
data MyMonad m where
MkMyMonad :: (Monad m) => MyMonad m
myReturn :: MyMonad m -> a -> m a
myReturn MkMyMonad = return
myBind :: MyMonad m -> m a -> (a -> m b) -> m b
myBind MkMyMonad = (>>=)
Note this may not yet be available in GHC CVS, see bug #1097046.
2. Casting among a limited set of types
data Witness a where
BoolWitness :: Witness Bool
IntWitness :: Witness Int
ListWitness :: Witness a -> Witness [a]
data ComposeT p q a = MkComposeT {unComposeT p (q a)}
witnessCast :: Witness a -> Witness b -> p a -> Maybe (p b)
witnessCast BoolWitness BoolWitness pa = Just pa;
witnessCast IntWitness IntWitness pa = Just pa;
witnessCast (ListWitness wa) (ListWitness wb) pla =
fmap unComposeT (witnessCast wa wb (MkComposeT pla))
witnessCast _ _ _ = Nothing;
class Castable a where
witness :: Witness a
instance Castable Bool where
witness = BoolWitness
instance Castable Int where
witness = IntWitness
instance (Castable a) => Castable [a] where
witness = ListWitness witness
cast :: (Castable a,Castable b) => p a -> Maybe (p b)
cast = witnessCast witness witness
castOne :: (Castable a,Castable b) => a -> Maybe b
castOne a = fmap runIdentity (cast (Identity a))
--
Ashley Yakeley, Seattle WA
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: The Implementation of Functional Programming Languages
On 8983 day of my life Simon Peyton-Jones wrote: > I'm happy to announce that my out-of-print 1987 book, > > The Implementation of Functional Programming Languages > > is now available online at > > http://research.microsoft.com/%7Esimonpj/papers/slpj-book-1987/index.htm > > Very many thanks to Marnie Montgomery, who did all the work. > > Happy reading That's wonderful!!! But I must admit that JPEG format is worst format for such publication. First, is blures images, that is OK for photos but very bad for texts. Second, it is not most compact format for black-and-white images. I tried to convert http://research.microsoft.com/%7Esimonpj/papers/slpj-book-1987/IMAGES/IV.JPG into different formats: 71626 Янв 9 00:35 IV.JPG-- original 10135 Янв 9 00:41 IV.png 5880 Янв 9 00:40 IV.djvu DjVu format is 12 times more compact, and PNG is 7 more compact!!! I would be glad to help you with converting files and explaining their advantages and disadvantages; feel free to contact me with e-mail. Note, however, that JPG images are not proper for conversion source because they are corrupted :( -- Ivan Boldyrev Outlook has performed an illegal operation and will be shut down. If the problem persists, contact the program vendor. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Guards (Was: Some random newbie questions)
Jon Cast wrote:
Absolutely. In Haskell's syntax, if-then-else-if interacts badly with
do notation, and Haskell lacks a direct analogy to Lisp's cond.
case () of
() | p1 -> e1
| p2 -> e2
...
No problem:
select :: a -> [(Bool, a)] -> a
select def = maybe def snd . List.find fst
Use it this way:
select defaultE
[(p1, e1),
(p2, e2)]
Would be a nice Prelude function.
parseCmd ln
| Left err <- parse cmd "Commands" ln
= BadCmd $ unwords $ lines $ show err
| Right x <- parse cmd "Commands" ln
= x
with the Haskell-98 alternative
parseCmd ln = case parse cmd "Commands" ln of
Left err -> BadCmd $ unwords $ lines $ show err
Right x -> x
Really, the second alternative is cleaner in my opinion.
Furthermore, guards are an extension of pattern matching, which means
you can write code like this:
xn !! n | n < 0 = error "Prelude.(!!): Negative index"
[] !! n = error "Prelude.(!!): Index overflow"
(x:xn) !! n | n == 0 = x
(x:xn) !! n = xn !! (n - 1)
Exactly one equation for each edge in the control-flow graph, which is
nice and not easily done (I'm not sure it's even possible) without
guards.
At least one guard can nicely be avoided:
(x:xn) !! n = if n == 0 then x else xn !! (n - 1)
But I see that guards can be used to let pattern matching fail.
Pattern guards are also nice for implementing ‘views’:
-- | Convert an 'XMLData' into an equivalent application of
-- 'Balanced', if possible. In any case, return an equivalent data
-- structure.
balance (Balanced es) = Balanced es
balance (LeftLeaning (LeftBalanced e:es))
| Balanced es' <- balance (LeftLeaning es)
= Balanced (e:es')
I don't know what this means exactly, but I think I can transform it
formally to:
balance e'@(LeftLeaning (LeftBalanced e:es)) =
case balance (LeftLeaning es) of
Balanced es' -> Balanced (e:es')
_ -> e'
This way it is more clear for me, that 'balance' can return something
different from 'Balanced' and that the data is returned unchanged in
this case.
balance (LeftLeaning []) = Balanced []
balance (RightLeaning [("", "", es)]) = Balanced es
balance (RightLeaning []) = Balanced []
balance e = e
Well, I could never do without them.
Sometimes I see people abusing guards, e.g. they write a 'length x == 1'
guard, where the pattern '[x0]' would be clearly the better choice. So
I'm always thinking twice before using a guard.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Some random newbie questions
Many thanks to everyone for the very helpful answers to my queries! - Benjamin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Hugs vs GHC (again) was: Re: Some random newbiequestions
On Sat, Jan 08, 2005 at 08:08:38AM +, Aaron Denney wrote: > I suppose I wouldn't be too upset at using the locale information, but > defaulting to UTF-8, rather than ASCII for unset character set > information. But if we default to a UTF-8 encoding, then there could be decoding failures when attempting to read a file. You have to consider both the possibility that characters aren't expressible in a given encoding and the possibility that files aren't expressible in a given encoding. ASCII (or iso-whatever) has the advantage that at least every file is readable. But as you say, really what we need is a binary IO system first, and then the character-based IO can do whatever it likes without breaking things (since it'll only be used by programs that actually want unicode coding). -- David Roundy http://www.darcs.net ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Hugs vs GHC (again) was: Re: Some random newbiequestions
On 2005-01-07, Simon Marlow <[EMAIL PROTECTED]> wrote: > - Can you use (some encoding of) Unicode for your Haskell source files? >I don't think this is true in any Haskell compiler right now. I assume this won't be be done until the next one is done... > - Can you do String I/O in some encoding of Unicode? No Haskell >compiler has support for this yet, and there are design decisions >to be made. Some progress has been made on an experimental prototype >(see recent discussion on this list). Many of the easy ways to do this that I've heard proposed make the current hacks for binary IO fail. IMHO, we really, really, need a standard, supported way to do binary IO. If I can read in and output octets, then I can implement unicode handling on top of that. In fact it would let a bunch of the proposed ideas for unicode support can be implemented in pure haskell and have API details hashed out and polished. For unix, there are couple different tacks one could take. The locale system is standard, and does work, but is ugly and a pain to work with. In particular, it's another (set of) global variables. And what do you do with a character not expressible in the current locale? I'd like to possibility of different character sets for different files, for example. I suppose I wouldn't be too upset at using the locale information, but defaulting to UTF-8, rather than ASCII for unset character set information. For win32, I really don't know the options. > - What about Unicode FilePaths? This was discussed a few months ago >on the haskell(-cafe) list, no support yet in any compiler. This is tricky, because most systems don't have such a thing terribly standard. For win32, it is standardized and should be wrappable fairly easily, but I don't know that I'd want to base my model on that. For unix, again, there is the locale system, with, again, the problem of unrepresentable characters. Traditionally systems have essentially said "file names are zero-terminated strings of bytes that may not contain character 47, which is used to seperate directory names", and the interpretation as a matter of _names_ and _characters_ was entirely a matter up to the terminals (or graphical programs, eventually) for display and programs for manipulation. -- Aaron Denney -><- ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
