examples/Demo.hs

   1 {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
   2 module Demo ({-sample1,sample2,-}sample5,sample6) where
   3
   4 sample5 :: forall c . (Int -> <{Int}>@c) ->  <{Int -> Int -> Int}>@c -> <{Int -> Int}>@c
   5 sample5 const <[ (*) ]> =
   6  <{ \y ->
   7     let   foo  = (~~(const 3) * foo) * y
   8     in    foo }>
   9
  10 sample6 :: forall c . (Int -> <{Int}>@c) -> <{Int -> Int -> Int}>@c -> <{Int -> Int}>@c
  11 sample6 const <{ (*) }> = pow 6
  12    where
  13      --pow :: Int -> <{ Int -> Int }>@a
  14      pow 0 = <{ \x -> ~~(const 1) }>
  15      pow 1 = <{ \x -> x }>
  16      pow n = <{ \x -> x * ~~(pow (n - 1)) x }>
  17
  18 demo2 ::
  19     forall c .
  20          (Int -> <{Int}>@c) ->
  21         <{Int -> Int -> Int}>@c ->
  22         <{Int -> Int}>@c
  23
  24 demo2 const mult =
  25   <{ \y ->
  26      ~~mult
  27        (~~(const 1))
  28        (~~mult y y)
  29    }>
  30
  31
  32
  33
  34
  35
  36
  37 {-
  38 demo const mult =
  39   <{ \y ->
  40      ~~mult
  41        (~~mult (~~mult y y) (~~mult y y))
  42        (~~mult (~~mult y y) (~~mult y y))
  43    }>
  44 -}
  45
  46
  47
  48 {-
  49 demo const mult =
  50     <{ \y -> ~~(foo 4) }>
  51         where
  52           foo 0 = const (12::Int)
  53           foo n = <{ let bar = ~~(foo (n-1))
  54                      in ~~mult bar bar
  55                    }>
  56
  57 -}
  58
  59
  60
  61 {-
  62 demo const mult =
  63     <{ \y -> ~~(foo 3) }>
  64         where
  65           foo 0 = const (12::Int)
  66           foo n = <{ let recurs = ~~(foo (n-1))
  67                      in  ~~mult recurs recurs
  68                    }>
  69
  70 -}
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86 {-
  87 demo const mult =
  88     <{ \y -> ~~(foo 2 <{y}>) }>
  89         where
  90           foo 0 y = const (12::Int)
  91           foo n y = <{ let recurs = ~~(foo (n-1) y)
  92                        in  ~~mult recurs recurs
  93                      }>
  94 -}
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130
 131
 132
 133
 134
 135
 136 -- demo const mult = <{ \(y::Int) -> ~~mult y ~~(const 12) }>
 137 -- demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) }>
 138 -- golden
 139 {-
 140 demo const mult =
 141  <{ \y ->
 142     let   twelve  = ~~mult twelve y
 143     in    twelve }>
 144 -}
 145
 146 {-
 147 demo const mult =
 148    <{ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) }>
 149 -}
 150
 151 {-
 152 demo const mult =
 153    <{ \(y::Int) ->
 154       let four   = ~~mult four ~~(const  4)
 155 --          twelve = {- {- ~~mult four -}  ~~(const 12) -} four
 156       in  four
 157     }>
 158 -}
 159
 160 {-
 161 demo const mult =
 162  <{ let     twelve = ~~(const (12::Int))
 163     in let  four    = ~~(const (4::Int))
 164          in  ~~mult four twelve  }>
 165 -}
 166
 167 {-
 168 demo const mult = demo' 3
 169  where
 170   demo' 0 = const 12
 171   demo' 1 = const 12
 172   demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) }>
 173 -}
 174
 175 -- BUG
 176 --demo const mult = <{ \y -> ~~(demo' 0) }>
 177 --  where
 178 --   demo' 0 = const 4
 179 --   demo' n = const 4