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
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
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
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
(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 -
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
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 =
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
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
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
{-# 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
-- 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
12 matches
Mail list logo
