@@ -0,0 +1,56 @@
3+data Free : (f : Type -> Type) -> (a : Type) -> Type where
5+ Bind : f (Free f a) -> Free f a
7+Functor f => Functor (Free f) where
8+ map f m = assert_total $ case m of
10+ Bind x => Bind (map (map f) x)
12+Functor f => Applicative (Free f) where
15+ m <*> x = assert_total $ case m of
17+ Bind f => Bind (map (<*> x) f)
19+Functor f => Monad (Free f) where
20+ m >>= f = assert_total $ case m of
22+ Bind x => Bind (map (>>= f) x)
24+liftFree : Functor f => f a -> Free f a
25+liftFree = assert_total $ Bind . map Pure
27+foldFree : (Monad m, Functor f) => ({ a : Type } -> f a -> m a) -> Free f b -> m b
28+foldFree f m = assert_total $ case m of
30+ Bind x => f x >>= foldFree f
33+ = ReadFile (String -> next)
35+FileSystem : Type -> Type
36+FileSystem = Free FileSystemF
38+Functor FileSystemF where
39+ map f (ReadFile nextFn) = ReadFile (f . nextFn)
41+readFileF : FileSystem String
42+readFileF = liftFree $ ReadFile id
46+interpret2 : FileSystemF a -> IO a
47+interpret2 (ReadFile nextFn) = do
48+ contents <- pure "ola"
49+ pure (nextFn contents)
54+ c <- foldFree interpret2 readFileF