Jan Christiansen wrote:
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
Nice, that is a lot simpler indeed, and even closer to the core of the idea.
Best regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe