Just for fun

2001-01-09 Thread Anton Moscal 

Hello!

This is well-known definition of the existential quantification through
universal:

(E x.P(x)) = A y.(A x.P (x) = y) = y

I try to translate in to Haskell. The following program can be compiled 
by "ghc -fglasgow-exts ..." and works correctly:


import Char

type E a = forall t . (forall x . a x - t) - t

newtype Pair a b = MkPair (b, (b - a))
newtype App  a   = MkApp  (E  (Pair a))

mk_app :: (a - b) - a - App b
mk_app f v = MkApp (\g - g (MkPair (v, f)))

app_s  = mk_app Char.ord '1'
app_id = mk_app (\x-x) 239

eval :: App a - a
eval (MkApp g) = g (\(MkPair (x, f)) - f x)

main = print (map eval [mk_app (\x-x) 239, mk_app Char.ord '1'])
---

Regards,
Anton Moscal


___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Just for fun

2001-01-09 Thread Tom Pledger 

Anton Moscal writes:
  Hello!
  
  This is well-known definition of the existential quantification
  through universal:
  
  (E x.P(x)) = A y.(A x.P (x) = y) = y
  
  I try to translate in to Haskell. The following program can be
  compiled by "ghc -fglasgow-exts ..." and works correctly:
  
 [...]
  main = print (map eval [mk_app (\x-x) 239, mk_app Char.ord '1'])



import Char(ord)

main = print (tail [error "I'm too lazy to be explicitly existential.",
(\x-x) 239,
ord '1'])

{- Regards, Tom :-}

___
Haskell mailing list
[EMAIL PROTECTED]
http://www.haskell.org/mailman/listinfo/haskell

Just for fun

2000-03-28 Thread Jerzy Karczmarczuk 

If you try to exercize some popular Web search engines on:

"Haskell Library"

you will get this: http://www.vtonly.com/hstydec9.htm

Perhaps we should send them the Report?

Jerzy Karczmarczuk
Caen, France.