Re: [Haskell-cafe] Existential question

[oleg]

 Ehm... what? How can you do such a replacement without losing, for
 example, functions like this:
 f (KI s h) i = snd $ h i $ fst $ h i s

Well, if we eliminate the existential from

   data Kl i o = forall s. Kl s (i -  s -  (s, o))

following strictly the procedure we obtain

data S i o = S (i - (S i o, o))

It is the data type of infinite streams, with an extra input. Your
function is obtaining the second element of the stream (assuming the
constant input i).  Infinite streams form a monad, as described in
great detail here:

http://patternsinfp.wordpress.com/2010/12/31/stream-monad/


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

Re: [Haskell-cafe] Existential question

[oleg]

 I had simplified the type to make the plumbing simpler.  My intention 
 was to include an initial value to use the function as a sequence 
 transformer / generator:

 data Kl i o = forall s. Kl s (i -  s -  (s, o))

That change makes a world of difference! For example, the above type
(Kl i) is clearly a monad

 instance Monad (Kl i) where
 return x = Kl () (\_ s - (s,x))
 (Kl s m) = f = Kl s (\i s - case f (snd (m i s)) of
  Kl s' m' - (s,snd (m' i s')))


It is the Reader monad. Different Kl values have their own, private s.
The quantification ensures that each encapsulated 's' applies only to
its generator. Therefore, we can just as well apply that 's' right at
the very beginning. Therefore,

 data Kl i o = forall s. Kl s (i -  s -  (s, o))

is essentially

 data Kl' i o = Kl' (i - o)

which is certainly and Arrow and a Monad. We do not need existential
at all. The web page
http://okmij.org/ftp/Computation/Existentials.html
describes other eliminations of Existentials.


 Does the growing type s1 - s2 - (s1,s2) in the bind-like method 
 below support some other abstraction that is monad-like?

 data Kl1' s o = Kl1' (s - (s,o))

 bind' :: (Kl1' s1 i) - (i - Kl1' s2 o) - (Kl1' (s1,s2) o)

 bind' mi f = Kl1' mo where
mo (s1,s2) = ((s1',s2'),o) where
  (Kl1' u1) = mi
  (s1', i)  = u1 s1
  (Kl1' u2) = f i
  (s2', o)  = u2 s2

Not all things are monads; for example, restricted and parameterized
monads are not monads (but do look like them, enough for the
do-notation). Your Kl1' does look like another generalization of
monads. I must say that it seems to me more fitting for a parametrized
applicative:

 class Appish i where
 purish :: a - i s a
 appish :: i s1 (a -b) - i s2 a - i (s1,s2) b

 data KL s a = KL (s - (s,a))

 instance Appish KL where
 purish x = KL (\s - (s,x))
 appish (KL f1) (KL f2) = KL $ \(s1,s2) -
   let (s1', ab) = f1 s1
   (s2', a)  = f2 s2
   in ((s1',s2'), ab a)


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

Re: [Haskell-cafe] Existential question

[MigMit]

Ehm... what? How can you do such a replacement without losing, for example, 
functions like this:

f (KI s h) i = snd $ h i $ fst $ h i s

Отправлено с iPad

24.08.2011, в 11:43, o...@okmij.org написал(а):

 
 I had simplified the type to make the plumbing simpler.  My intention 
 was to include an initial value to use the function as a sequence 
 transformer / generator:
 
 data Kl i o = forall s. Kl s (i -  s -  (s, o))
 
 That change makes a world of difference! For example, the above type
 (Kl i) is clearly a monad
 
 instance Monad (Kl i) where
return x = Kl () (\_ s - (s,x))
(Kl s m) = f = Kl s (\i s - case f (snd (m i s)) of
   Kl s' m' - (s,snd (m' i s')))
 
 
 It is the Reader monad. Different Kl values have their own, private s.
 The quantification ensures that each encapsulated 's' applies only to
 its generator. Therefore, we can just as well apply that 's' right at
 the very beginning. Therefore,
 
 data Kl i o = forall s. Kl s (i -  s -  (s, o))
 
 is essentially
 
 data Kl' i o = Kl' (i - o)
 
 which is certainly and Arrow and a Monad. We do not need existential
 at all. The web page
http://okmij.org/ftp/Computation/Existentials.html
 describes other eliminations of Existentials.
 
 
 Does the growing type s1 - s2 - (s1,s2) in the bind-like method 
 below support some other abstraction that is monad-like?
 
 data Kl1' s o = Kl1' (s - (s,o))
 
 bind' :: (Kl1' s1 i) - (i - Kl1' s2 o) - (Kl1' (s1,s2) o)
 
 bind' mi f = Kl1' mo where
   mo (s1,s2) = ((s1',s2'),o) where
 (Kl1' u1) = mi
 (s1', i)  = u1 s1
 (Kl1' u2) = f i
 (s2', o)  = u2 s2
 
 Not all things are monads; for example, restricted and parameterized
 monads are not monads (but do look like them, enough for the
 do-notation). Your Kl1' does look like another generalization of
 monads. I must say that it seems to me more fitting for a parametrized
 applicative:
 
 class Appish i where
purish :: a - i s a
appish :: i s1 (a -b) - i s2 a - i (s1,s2) b
 
 data KL s a = KL (s - (s,a))
 
 instance Appish KL where
purish x = KL (\s - (s,x))
appish (KL f1) (KL f2) = KL $ \(s1,s2) -
  let (s1', ab) = f1 s1
  (s2', a)  = f2 s2
  in ((s1',s2'), ab a)
 
 
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

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

Re: [Haskell-cafe] Existential question

[Tom Schouten]

On 08/21/2011 05:33 AM, Felipe Almeida Lessa wrote:

On Sat, Aug 20, 2011 at 6:26 PM, Tom Schoutent...@zwizwa.be  wrote:

data Kl i o = forall s. Kl s (i -s -(s, o))

This is an Arrow.  At first I wondered if there was also an associated
Monad, hence the iso function.

Given

   data Kl i o = forall s. Kl s (i -s -(s, o))

   instance ArrrowApply KI where
 ...

then 'ArrowMonad KI' [1] is a monad isomorphic to

   data KIM o = forall s. KIM s (s -  (s, o))

Is this what you are looking for?


Yes, but I run into the same problem.


data Kl i o = forall s. Kl (i - s - (s, o))

-- OK
instance Category Kl where
  id = Kl $ \ i () - ((), i)
  (.) (Kl u2) (Kl u1) = (Kl u12) where
u12 a (s1, s2) = ((s1',s2'), c) where
  (s1', b) = u1 a s1
  (s2', c) = u2 b s2

-- OK
instance Arrow Kl where
  arr f = Kl $ \i () - ((), f i)
  first (Kl u) = (Kl u') where
u' (i, x) s = (s', (o, x)) where
  (s', o) = u i s

-- Can't make this work.  The problem seems to be the same as before:
-- there's no way to require that the hidden types of both Kl
-- constructors are the same.
instance ArrowApply Kl where
  app = Kl $ \((Kl f), a) - f a


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

Re: [Haskell-cafe] Existential question

[Felipe Almeida Lessa]

(Code from this e-mail attached.)

On Sun, Aug 21, 2011 at 7:22 AM, Tom Schouten t...@zwizwa.be wrote:
 Yes, but I run into the same problem.

 data Kl i o = forall s. Kl (i - s - (s, o))

You actually forgot the 's' field of KI in my e-mail.  If you define

  data KI i o = forall s. KI s (i - s - (s, o))
  instance Category KI where ...
  instance Arrow KI where ...

You can make

  instance ArrowApply KI where
  app = KI () $ \(KI s u, b) _ - ((), snd $ u b s)

But this is probably very uninteresting, since the state is just thrown away.

However, if you used

  data KIT i o = forall s. Typeable s = KIT s (i - s - (s, o))
  instance Category KIT where ...
  instance Arrow KIT where ...

You could make

  instance ArrowApply KIT where
  app = KIT (toDyn ()) $
  \(KIT s u, b) dyn - first toDyn $ u b (fromDyn dyn s)

This app operator behaves as KI's app when the argument is not very
well behaving (i.e. changing the state type).  However, when the
argument does behave well, it is given the associated state only once.
 All further iterations work as they should.

Note that since ArrowApply is equivalent to Monad, you may also try
going the other way around.  That is, define

  data KIM o = forall s. KIM s (s - (s, o))

  instance Monad KIM where
  return x = KIM () $ \_ - ((), x)
  KIM sx ux = f = KIM sx u
  where
u sx' = let (tx, i) = ux sx'
in case f i of
 KIM sf uf - let (_, o) = uf sf
  in (tx, o)

I haven't checked, but I think that 'Kleisli KIM' is isomorphic to
'KI', and that 'ArrowMonad KI' is isomorphic to 'KIM'.

You may also define

  data KIMT o = forall s. Typeable s = KIMT s (s - (s, o))

  instance Monad KIMT where
  return x = KIMT () $ \_ - ((), x)
  KIMT sx ux = f = KIMT (sx, toDyn ()) u
  where
u (sx', dyn) = let (tx, i) = ux sx'
   in case f i of
KIMT sf uf -
let (tf,  o) = uf (fromDyn dyn sf)
in ((tx, toDyn tf), o)

And the same conjecture applies between 'Kleisli KIMT' and 'KIT', and
between 'KIMT' and 'ArrowMonad KIT'.

Conclusion: Data.Typeable lets you cheat =).

Cheers,

-- 
Felipe.
{-# LANGUAGE ExistentialQuantification #-}

import Prelude hiding (id, (.))
import Control.Arrow
import Control.Category
import Data.Typeable
import Data.Dynamic

--

data KI i o = forall s. KI s (i - s - (s, o))

instance Category KI where
id = arr id
KI s2 u2 . KI s1 u1 = KI s u
  where
s = (s2, s1)
u = \i1 (s2', s1') - let (t1, i2) = u1 i1 s1'
  (t2, o)  = u2 i2 s2'
  in ((t2, t1), o)

instance Arrow KI where
arr f = KI () $ \i _ - ((), f i)
first (KI s u) = KI s $ \(b, d) s - let (t, c) = u b s
in (t, (c, d))

instance ArrowApply KI where
app = KI () $ \(KI s u, b) _ - ((), snd $ u b s)

type KI_M = ArrowMonad KI

--

data KIT i o = forall s. Typeable s = KIT s (i - s - (s, o))

instance Category KIT where
id = arr id
KIT s2 u2 . KIT s1 u1 = KIT s u
  where
s = (s2, s1)
u = \i1 (s2', s1') - let (t1, i2) = u1 i1 s1'
  (t2, o)  = u2 i2 s2'
  in ((t2, t1), o)

instance Arrow KIT where
arr f = KIT () $ \i _ - ((), f i)
first (KIT s u) = KIT s $ \(b, d) s - let (t, c) = u b s
in (t, (c, d))

instance ArrowApply KIT where
app = KIT (toDyn ()) $
\(KIT s u, b) dyn - first toDyn $ u b (fromDyn dyn s)

type KIT_M = ArrowMonad KIT

--

data KIM o = forall s. KIM s (s - (s, o))

instance Monad KIM where
return x = KIM () $ \_ - ((), x)
KIM sx ux = f = KIM sx u
where
  u sx' = let (tx, i) = ux sx'
  in case f i of
   KIM sf uf - let (_, o) = uf sf
in (tx, o)

type KIM_A = Kleisli KIM

--

data KIMT o = forall s. Typeable s = KIMT s (s - (s, o))

instance Monad KIMT where
return x = KIMT () $ \_ - ((), x)
KIMT sx ux = f = KIMT (sx, toDyn ()) u
where
  u (sx', dyn) = let (tx, i) = ux sx'
 in case f i of
  KIMT sf uf -
  let (tf,  o) = uf (fromDyn dyn sf)
  in ((tx, toDyn tf), o)

type KIMT_A = Kleisli KIMT
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org

Re: [Haskell-cafe] Existential question

[Tom Schouten]

On 08/19/2011 08:50 AM, Ryan Ingram wrote:


ki1 :: KI () Int
ki1 = KI @Int (\() s - (s+1, s))

ki2 :: KI () Int
ki2 = KI @() (\() () - ((), 0))

f :: Bool - KI () Int
f x = if x then ki1 else ki2

iso f = KI ?? ??

The problem is that we have multiple possible internal state types!


Aha!
Nice counterexample.
Thanks :)


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

Re: [Haskell-cafe] Existential question

[Tom Schouten]

On 08/18/2011 07:27 AM, o...@okmij.org wrote:

-- Is there a way to make this one work also?
data Kl i o = forall s. Kl (i -  s -  (s, o))
iso :: (i -  Kl () o) -  Kl i o
iso f = Kl $ \i s -  (\(Kl kl) -  kl () s) (f i)

Yes, if you move the quantifier:

type Kl i o = i -  Kl1 o
data Kl1 o = forall s. Kl1 (s -  (s,o))
iso :: (i -  Kl () o) -  Kl i o
iso f = \i -  f i ()

iso1 :: Kl i o -  (i -  Kl () o)
iso1 f = \i -  (\() -  f i)


Thanks, Oleg.


I'm not sure if it helps in the long run: the original Kl and mine Kl1
are useless. Suppose we have the value kl1 :: Kl Int Bool
with the original declaration of Kl:

data Kl i o = forall s. Kl (i -  s -  (s, o))

I had simplified the type to make the plumbing simpler.  My intention 
was to include an initial value to use the function as a sequence 
transformer / generator:


data Kl i o = forall s. Kl s (i -  s -  (s, o))


This is an Arrow.  At first I wondered if there was also an associated 
Monad, hence the iso function.  From your reply and Ryan's comment it 
seems that making a Monad instance for


data Kl1 o = forall s. Kl (s - (s,o))

is not possible because its bind function cannot be typed as the (i - 
Kl1 o) function introduces a value - type dependency.



Does the growing type s1 - s2 - (s1,s2) in the bind-like method 
below support some other abstraction that is monad-like?


data Kl1' s o = Kl1' (s - (s,o))

bind' :: (Kl1' s1 i) - (i - Kl1' s2 o) - (Kl1' (s1,s2) o)

bind' mi f = Kl1' mo where
  mo (s1,s2) = ((s1',s2'),o) where
(Kl1' u1) = mi
(s1', i)  = u1 s1
(Kl1' u2) = f i
(s2', o)  = u2 s2


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

Re: [Haskell-cafe] Existential question

[Felipe Almeida Lessa]

On Sat, Aug 20, 2011 at 6:26 PM, Tom Schouten t...@zwizwa.be wrote:
 data Kl i o = forall s. Kl s (i -  s -  (s, o))

 This is an Arrow.  At first I wondered if there was also an associated
 Monad, hence the iso function.

Given

  data Kl i o = forall s. Kl s (i -  s -  (s, o))

  instance ArrrowApply KI where
...

then 'ArrowMonad KI' [1] is a monad isomorphic to

  data KIM o = forall s. KIM s (s - (s, o))

Is this what you are looking for?

Cheers! =)

[1] 
http://hackage.haskell.org/packages/archive/base/4.3.1.0/doc/html/Control-Arrow.html#t:ArrowMonad

-- 
Felipe.

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

Re: [Haskell-cafe] Existential question

[Ryan Ingram]

On Wed, Aug 17, 2011 at 4:49 PM, Tom Schouten t...@zwizwa.be wrote:

 {-# LANGUAGE ExistentialQuantification #-}

 -- Dear Cafe, this one works.
 data Kl' s i o = Kl' (i - s - (s, o))
 iso' :: (i - Kl' s () o) - Kl' s i o
 iso' f = Kl' $ \i s - (\(Kl' kl') - kl' () s) (f i)

 -- Is there a way to make this one work also?
 data Kl i o = forall s. Kl (i - s - (s, o))
 iso :: (i - Kl () o) - Kl i o
 iso f = Kl $ \i s - (\(Kl kl) - kl () s) (f i)


Not without moving the quantifier, as Oleg says.  Here is why:

Existential types are equivalent to packing up a type with the constructor;
imagine KI as

data KI i o = KI @s (i - s - (s,o))   -- not legal haskell

where @s represents hold a type s which can be used in the other elements
of the structure.  An example element of this type:

  KI @[Int] (\i s - (i:s, sum s)) :: KI Int Int

Trying to implement iso as you suggest, we end up with

iso f = KI ?? (\i s - case f i of ...)

What do we put in the ??.  In fact, it's not possible to find a solution;
consider this:

ki1 :: KI () Int
ki1 = KI @Int (\() s - (s+1, s))

ki2 :: KI () Int
ki2 = KI @() (\() () - ((), 0))

f :: Bool - KI () Int
f x = if x then ki1 else ki2

iso f = KI ?? ??

The problem is that we have multiple possible internal state types!

  -- ryan


 {-
Couldn't match type `s0' with `s'
  because type variable `s' would escape its scope
This (rigid, skolem) type variable is bound by
  a pattern with constructor
Kl :: forall i o s. (i - s - (s, o)) - Kl i o,
  in a lambda abstraction
The following variables have types that mention s0
  s :: s0 (bound at /home/tom/meta/haskell/iso.hs:**11:17)
In the pattern: Kl kl
In the expression: \ (Kl kl) - kl () s
In the expression: (\ (Kl kl) - kl () s) (f i)
 -}


 __**_
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/**mailman/listinfo/haskell-cafehttp://www.haskell.org/mailman/listinfo/haskell-cafe

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

Re: [Haskell-cafe] Existential question

[Miguel Mitrofanov]

 Now, what we can do with kl1? We can feed it an integer, say 1, and
 obtain function f of the type s - (s,Bool) for an _unknown_ type s.
 Informally, that type is different from any concrete type. We can
 never find the Bool result produced by that function since we can
 never have any concrete value s. The only applications of f that will
 type check are
   \s - f s
   f undefined
 both of which are useless to obtain f's result.

That's not true. We can tie the knot:

let (s, o) = f s in o


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

Re: [Haskell-cafe] Existential question

[oleg]

 -- Is there a way to make this one work also?
 data Kl i o = forall s. Kl (i - s - (s, o))
 iso :: (i - Kl () o) - Kl i o
 iso f = Kl $ \i s - (\(Kl kl) - kl () s) (f i)

Yes, if you move the quantifier:

type Kl i o = i - Kl1 o
data Kl1 o = forall s. Kl1 (s - (s,o))
iso :: (i - Kl () o) - Kl i o
iso f = \i - f i ()

iso1 :: Kl i o - (i - Kl () o)
iso1 f = \i - (\() - f i)


I'm not sure if it helps in the long run: the original Kl and mine Kl1
are useless. Suppose we have the value kl1 :: Kl Int Bool 
with the original declaration of Kl:

data Kl i o = forall s. Kl (i - s - (s, o))

Now, what we can do with kl1? We can feed it an integer, say 1, and
obtain function f of the type s - (s,Bool) for an _unknown_ type s.
Informally, that type is different from any concrete type. We can
never find the Bool result produced by that function since we can
never have any concrete value s. The only applications of f that will
type check are
\s - f s
f undefined
both of which are useless to obtain f's result.





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