blob: 0caa84cbe18dd38bc88ceb8e9fa5025afcd67294 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
{-# OPTIONS_GHC -XImpredicativeTypes -fno-warn-deprecated-flags -XEmptyDataDecls -XGADTs #-}
-- Trac #1118
module Compose where
data Z
data S n
data List n a where
Nil :: List Z a
(:-) :: a -> List n a -> List (S n) a
data Hold a = Hold (forall m . a m -> a (S m))
compose' :: List n (Hold a) -> a (S Z) -> a (S n)
compose' Nil x = x
compose' ((Hold f) :- fs) x = f (compose' fs x)
compose :: List n (forall m . a m -> a (S m)) -> a (S Z) -> a (S n)
compose Nil x = x
compose (f :- fs) x = f (compose fs x)
composeS :: [forall m . a m -> a m] -> a n -> a n
composeS [] x = x
composeS (f:fs) x = f (composeS fs x)
|
