2011-09-06.txt:06:28:10: <zzo38> If I explicit forall will it work?
2011-09-11.txt:22:45:28: <zzo38> Are church numerals the only function of type   forall a. (a -> a) -> a -> a   ?
2011-10-12.txt:04:15:23: <zzo38> The word "forall", "qualified", and "hiding" have special meanings in some cases, but it would not be ambiguous to use them in expressions since the special meanings of those words are not for expressions
2011-11-02.txt:23:05:11: <zzo38> Would it even be possible to make Haskell have a bijective function type <-> that you could, in addition to possibly conversion of some reversible esolangs, also be able to prove things such as:   forall a b c n. Not (Either (Maybe (Maybe (Maybe n)) -> Maybe a) (Maybe (Maybe (Maybe n)) -> Maybe b) <-> (Maybe (Maybe (Maybe n)) -> Maybe c))
2011-11-28.txt:06:52:27: <zzo38> explosion :: (p, Not p) -> q; explosion (x, y) = contradiction $ y x;     where    contradiction :: forall t. Zero -> t;
2011-11-28.txt:07:18:55: <zzo38> In TNT, (exist a. x) is equivalent to (not (forall a. not x))
2011-12-04.txt:23:16:50: <zzo38> Is this OK?   class Classical x => IsNatural x where { selfEqual :: x :=: x; induction :: (forall y. IsNatural y => f y -> f (Maybe y)) -> f Zero -> f x; };
2011-12-24.txt:09:39:43: <zzo38> I was trying to think of some kind of "IO transformer", but I don't know for sure. One thing I was think of is: newtype IOT f x = IOT (forall z. (f x -> IO z) -> IO z);
2012-01-04.txt:08:50:28: <zzo38> I try to make (Functor (forall x y. f x y)) to be a constraint but it doesn't seems to work
2012-01-29.txt:17:18:07: <zzo38> The contrapositive form of a monad m is (forall z. (x -> z) -> m z) which can join, but the form with w in it is (forall z. (x -> w z) -> m z) can they join (if w is a comonad)?
2012-01-29.txt:17:43:59: <zzo38> newtype T f x = T { runT :: forall z. (x -> z) -> f z }; fmap f (T x) = T $ \y -> x (y . f); join x = T $ \y -> join $ (runT (runT <$> x)) ($ y);
2012-02-09.txt:02:15:35: <zzo38> It is defined as    data DSum tag = forall a. !(tag a) :=> a
2012-02-09.txt:03:09:31: <zzo38> There is dependent sum type but another idea would be to have a constrainted dependent sum type:   data CDSum con tag = forall a. con a => !(tag a) :+> a;
2012-02-09.txt:05:44:30: <zzo38> newtype ExtProd p = ExtProd { getExtProd :: forall a. ExtProdC p a => a -> ExtProdF a };
2012-03-11.txt:10:57:07: <zzo38> class EphemerisClass x where { openEphemeris :: String -> IO x; closeEphemeris :: x -> IO (); accessEphemeris :: EphTime -> ObjMajor -> ObjMinor -> x -> IO (Either EphemerisError (XYZ, XYZ, XYZ)); }; data Ephemeris = Ephemeris { getEphemeris :: forall x. EphemerisClass x => x };    might be specification of this interface in Haskell.
2012-03-18.txt:20:09:07: <zzo38> Do you know if there is anything adding some function to Haskell "gloss" library that can have I/O action inside of something such as:  playIO :: forall x y. Display -> Color -> Int -> x -> (x -> Picture) -> (Event -> x -> IO (Either y x)) -> (Float -> x -> IO (Either y x)) -> IO y;
2012-03-31.txt:07:10:21: <zzo38> Can they implement Haskell Dynamic like that?   data Dynamic where { Dynamic :: forall x. Typeable x => x -> Dynamic; }; castDyn :: Typeable x => Dynamic -> Maybe x; castDyn (Dynamic x) = cast x;
2012-04-07.txt:23:54:56: <zzo38> class Typeable x => NodeClass x where { ... traverseBox :: (Applicative f, Monad f) => (Node -> f Node) -> x -> f Node; ... }; ... data Node where { Node :: forall x. NodeClass x => x -> Node; } deriving Typeable;
2012-04-08.txt:04:23:37: <zzo38> It seem like, LogicT is like a list with able to put (forall r. m r -> m r) stuff in between and at the end
2012-04-10.txt:19:16:34: <zzo38> In case we have something, like LogicT, but instead there is also a comonad included    (forall r. (a -> w (m r) -> m r) -> w (m r) -> m r)   It is still a codensity monad too
2012-04-16.txt:01:03:27: <zzo38> shachaf: Also, I have used something like that in my dvi-processing program, where   data Node where { Node :: forall x. NodeClass x => x -> Node; } deriving Typeable;   where NodeClass has Typeable as a superclass.
2012-04-18.txt:19:36:29: <zzo38> newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b } 
2012-04-19.txt:02:37:52: <zzo38> Is it a proper comonad?  data LeftCo m f x = forall z. LeftCo (f (m z) -> x) (f z); fmap f (LeftCo x y) = LeftCo (f . x) y; duplicate (LeftCo x y) = LeftCo (LeftCo (x . fmap join)) y; extract (LeftCo x y) = x (return <$> y);
2012-05-07.txt:08:24:55: <zzo38> I am using the DSum type from "dependent-sum" package; it is defined as follows:   data DSum tag = forall a. !(tag a) :=> a
2012-05-08.txt:01:24:22: <zzo38> data LeftCo m f x = forall z. LeftCo (f (m z) -> x) (f z);   If m is monad, does this make a comonad?   If m is monad, does this make a comonad transformer?
2012-05-25.txt:10:15:47: <zzo38> It doesn't seem possible to make it to add rows and columns to any type; but there are ways to do something close for specific purposes, one thing is object-oriented but there are other things too, possibly some things in "extensible-data" package might help in some cases, and maybe other uses of Typeable class such as:  data Xyz where { Xyz :: forall x. XyzClass x => x -> Xyz; } deriving Typeable; class Typeable x => XyzClass x where { ... };
2012-05-26.txt:23:03:23: <zzo38> I have thought of things like that too; with things like (forall x. x -> x -> x -> x -> x -> x) the cardinality is how many -> there are. And do you know what kind of function (forall x. [x] -> Maybe x) is?
2012-06-08.txt:03:51:40: <zzo38> Do you know if   data LeftCoT m f x = forall z. LeftCo (f (m z) -> x) (f z);   is a comonad? Do you know if it is a comonad transformer?
2012-06-08.txt:05:48:03: <zzo38> newtype Codensity f x = Codensity (forall z. (x -> f z) -> f z); newtype Endo x = Endo (x -> x);
2012-06-08.txt:05:50:48: <zzo38> oklopol: Fold function for a list [x] would be of type (forall z. (x -> z -> z) -> z -> z)
2012-06-29.txt:16:04:59: <zzo38> In Haskell (I have discussed this in #haskell channel yesterday), I have thought of (forall z. c z => (x -> z) -> z) and (forall z. c z => (z -> x, z)). The first one is right and the second one is left. Here I am using the methods and the mathematical laws of the class c.
2012-07-06.txt:22:39:36: <zzo38> I think this can make a MonadPlus whenever w is a comonad:   newtype CodensityAsk w x = CodensityAsk { runCodensityAsk :: forall z. w z -> (x -> z) -> z };   (and that it seems to always make a monad)
2012-07-08.txt:00:13:10: <zzo38> I have made up some functions for dealing with free monads, such as:   affectFree :: Functor g => (forall z. (s, f z) -> g (s, z)) -> (s, Free f x) -> Free g (s, x);   reduceFree :: Monad m => (forall z. f z -> m z) -> Free f x -> m x;
2012-07-08.txt:03:03:03: <zzo38> Do you know this one?   data Y :: ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> * -> * where { Y :: forall (w :: (* -> *) -> (* -> *) -> * -> *) (x :: * -> *) y z. w x y (x z) -> Y w y z; };
2012-07-08.txt:04:09:30: <zzo38> data X :: (* -> *) -> (* -> *) -> * -> * where { X :: y z -> X x y (x z); }; data Y :: ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> * -> * where { Y :: forall (w :: (* -> *) -> (* -> *) -> * -> *) (x :: * -> *) y z. w x y (x z) -> Y w y z; };
2012-07-08.txt:05:04:03: <zzo38> I did not post the CodensityAskT on here so now I will:  newtype CodensityAskT w m x = CodensityAskT { runCodensityAskT :: forall z. w (m z) -> (x -> m z) -> m z };
2012-07-08.txt:16:58:09: <zzo38> Do you have ideas to name   data X :: (* -> *) -> (* -> *) -> * -> * where { X :: y z -> X x y (x z); };   data Y :: ((* -> *) -> (* -> *) -> * -> *) -> (* -> *) -> * -> * where { Y :: forall (w :: (* -> *) -> (* -> *) -> * -> *) (x :: * -> *) y z. w x y (x z) -> Y w y z; };
2012-08-24.txt:02:54:33: <zzo38> newtype CodensityAsk f x = CodensityAsk { runCodensityAsk :: forall z. f z -> (x -> z) -> z };
2012-09-19.txt:01:10:11: <zzo38> data T x y = T (forall y. x y -> y);    Would something like this to do something?
2012-09-19.txt:01:12:22: <zzo38> I meant:    data T x = T (forall y. x y -> y);
2012-09-27.txt:03:20:56: <zzo38> newtype Codensity f x = Codensity (forall z. (x -> f z) -> f z);
2012-10-12.txt:01:04:33: <zzo38> Does this Haskell type meaningful anything to you (I wrote it while trying to figure out something else):  (forall y. forall z r. (x -> Cont r z) -> Cont r ((z -> x') -> y)) -> y)
2012-11-02.txt:22:27:17: <zzo38> But I thought it was something like, newtype Bazaar a b t = Bazaar { _runBazaar :: forall f. Applicative f => (a -> f b) -> f t } being the right bazaar and data Bazaar a b t = forall n : Nat. Bazaar ((n -> b) -> t) (n -> a) being the left bazaar, or something like that.
2013-02-07.txt:01:06:37: <HackEgo> 01:03:48: <zzo38> Now is this good enough, do you think so? \ 01:03:52: <zzo38> ?messages \ 01:03:52: <lambdabot> shachaf said 1d 4h 20m 13s ago: CodensityAsk reminds me of type MendlerAlgebra f c = forall a. (a -> c) -> f a -> c (except that it's different) \ 01:04:27: <shachaf> hi lambdabot \ 01:05:07: <tswett> zzo38: mm, thinking carefully about
2013-03-04.txt:22:09:12: <zzo38> forall p and q: B(p -> q) -> B(Bp -> Bq)
2013-03-08.txt:03:46:18: <oerjan> `pastequotes zzo38>.*forall
2013-03-08.txt:03:46:28: <oerjan> `pastelogs zzo38>.*forall