Hi, On Jan 2, 2012, at 2:34 PM, Heinrich Apfelmus wrote:
> Without an explicit guarantee that the function is incremental, we can't do > anything here. But we can just add another constructor to that effect if we > turn ListTo into a GADT: > > data ListTo a b where > CaseOf :: b -> (a -> ListTo a b) -> ListTo a b > Fmap :: (b -> c) -> ListTo a b -> ListTo a c > > FmapCons :: b -> ListTo a [b] -> ListTo a [b] I did not follow your discussion but how about using an additional GADT for the argument of Fmap, that is data Fun a b where Fun :: (a -> b) -> Fun a b Cons :: a -> Fun [a] [a] data ListTo a b where CaseOf :: b -> (a -> ListTo a b) -> ListTo a b Fmap :: Fun b c -> ListTo a b -> ListTo a c and provide a function to interpret this data type as well interpretFun :: Fun a b -> a -> b interpretFun (Fun f) = f interpretFun (Cons x) = (x:) for the sequential composition if I am not mistaken. (<.) :: ListTo b c -> ListTo a [b] -> ListTo a c (CaseOf _ cons) <. (Fmap (Cons y) b) = cons y <. b (Fmap f a) <. (Fmap g b) = Fmap f $ a <. (Fmap g b) a <. (CaseOf nil cons) = CaseOf (interpret a nil) ((a <.) . cons) a <. (Fmap f b) = fmap (interpret a . interpretFun f) b -- functor instance instance Functor (ListTo a) where fmap f = normalize . Fmap (Fun f) normalize :: ListTo a b -> ListTo a b normalize (Fmap (Fun f) (Fmap (Fun g) c)) = fmap (f . g) c normalize x = x Cheers, Jan _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
