examples/Demo.hs

   1 {-# OPTIONS_GHC -XModalTypes -fflatten -funsafe-skolemize -dcore-lint -XScopedTypeVariables -fsimpleopt-before-flatten #-}
   2 module Demo (demo) where
   3
   4 {-
   5 demo const mult =
   6   <{ \y ->
   7      ~~mult
   8        (~~mult y y)
   9        (~~mult y y)
  10    }>
  11 -}
  12
  13
  14
  15
  16
  17
  18 {-
  19 demo const mult =
  20   <{ \y ->
  21      ~~mult
  22        (~~mult (~~mult y y) (~~mult y y))
  23        (~~mult (~~mult y y) (~~mult y y))
  24    }>
  25 -}
  26
  27
  28
  29 {-
  30 demo const mult =
  31     <{ \y -> ~~(foo 4) }>
  32         where
  33           foo 0 = const (12::Int)
  34           foo n = <{ let bar = ~~(foo (n-1))
  35                      in ~~mult bar bar
  36                    }>
  37
  38 -}
  39
  40
  41
  42 {-
  43 demo const mult =
  44     <{ \y -> ~~(foo 3) }>
  45         where
  46           foo 0 = const (12::Int)
  47           foo n = <{ let recurs = ~~(foo (n-1))
  48                      in  ~~mult recurs recurs
  49                    }>
  50
  51 -}
  52
  53
  54
  55
  56
  57 demo const mult =
  58  <{ \y ->
  59     let   foo  = ~~mult (~~mult foo (~~mult y foo)) y
  60     in    foo }>
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73 {-
  74 demo const mult =
  75     <{ \y -> ~~(foo 2 <{y}>) }>
  76         where
  77           foo 0 y = const (12::Int)
  78           foo n y = <{ let recurs = ~~(foo (n-1) y)
  79                        in  ~~mult recurs recurs
  80                      }>
  81 -}
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  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 -- demo const mult = <{ \(y::Int) -> ~~mult y ~~(const 12) }>
 124 -- demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-1)) }>
 125 -- golden
 126 {-
 127 demo const mult =
 128  <{ \y ->
 129     let   twelve  = ~~mult twelve y
 130     in    twelve }>
 131 -}
 132
 133 {-
 134 demo const mult =
 135    <{ \y -> let y = ~~(const 4) in ~~mult (~~mult y y) (~~mult y y) }>
 136 -}
 137
 138 {-
 139 demo const mult =
 140    <{ \(y::Int) ->
 141       let four   = ~~mult four ~~(const  4)
 142 --          twelve = {- {- ~~mult four -}  ~~(const 12) -} four
 143       in  four
 144     }>
 145 -}
 146 demo ::
 147     forall c .
 148          (Int -> <{Int}>@c) ->
 149         <{Int -> Int -> Int}>@c ->
 150         <{Int -> Int}>@c
 151
 152 {-
 153 demo const mult =
 154  <{ let     twelve = ~~(const (12::Int))
 155     in let  four    = ~~(const (4::Int))
 156          in  ~~mult four twelve  }>
 157 -}
 158
 159 {-
 160 demo const mult = demo' 3
 161  where
 162   demo' 0 = const 12
 163   demo' 1 = const 12
 164   demo' n = <{ ~~mult ~~(demo' (n-1)) ~~(demo' (n-2)) }>
 165 -}
 166
 167 -- BUG
 168 --demo const mult = <{ \y -> ~~(demo' 0) }>
 169 --  where
 170 --   demo' 0 = const 4
 171 --   demo' n = const 4