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
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
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
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
|
{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, StandaloneDeriving, TypeFamilies, GADTs
, ViewPatterns, TypeOperators, TypeApplications, StandaloneDeriving
, UnicodeSyntax, PatternSynonyms, FlexibleContexts, DataKinds, UndecidableInstances
, TypeFamilyDependencies #-}
-- invoke as: ghci Main.hs -ddump-parsed -ddump-rn
-- or in GHCi: :set -ddump-parsed -ddump-rn
import TyFamWitnesses
import Language.Haskell.TH hiding (Type)
import Data.Type.Equality hiding (apply)
import Type.Reflection
import Unsafe.Coerce (unsafeCoerce)
import Data.Char (ord)
import GHC.TypeLits
stuffhave = [d| type family Foo a b where
Foo a a = Int
Foo (IO a) a = Float
Foo (IO a) b = Bool
Foo a Char = String
Foo a b = Char |]
stuffhave1 = [d| type family Bar a where Bar Bool = Bool; Bar a = IO a |]
stuffhave2 = [d| type family Elim a b where Elim a (a -> b) = b; Elim a (c -> b) = c -> Elim a b |]
witnesses [d| type family Foo a b where
Foo a a = Int
Foo (IO a) a = Float
Foo (IO a) b = Bool
Foo a Char = String
Foo a b = Char |]
deriving instance Show (FooRefl a b)
-- now you can:
--
-- >>> :info FooRefl
-- type role FooRefl nominal nominal
-- data FooRefl a b where
-- Foo0 :: (Foo a a ~ Int) => FooRefl a a
-- Foo1 :: (Foo (IO b) b ~ Float) => FooRefl (IO b) b
-- Foo2 :: (Foo (IO a1) b ~ Bool) => FooRefl (IO a1) b
-- Foo3 :: (Foo a Char ~ String) => FooRefl a Char
-- Foo4 :: (Foo a b ~ Char) => FooRefl a b
-- -- Defined at Main.hs:13:1
-- instance Show (FooRefl a b) -- Defined at Main.hs:14:1
--
-- >>> :info reify_Foo
-- reify_Foo :: TypeRep a -> TypeRep b -> Maybe (FooRefl a b)
-- -- Defined at Main.hs:13:1
--
-- >>> reify_Foo (typeOf getChar) (typeRep @Char)
-- Just Foo1
--
witnesses [d| type family Bar a where Bar Bool = Bool; Bar a = IO a |]
deriving instance Show (BarRefl a)
witnesses [d| type family Elim a b where Elim a (a -> b) = b; Elim a (c -> b) = c -> Elim a b |]
deriving instance Show (ElimRefl a b)
pure []
stuffwant2 = [d|
fooRefl :: forall a b . TypeRep a -> TypeRep b -> Maybe (FooRefl a b)
fooRefl a b | Just HRefl <- eqTypeRep a b = pure Foo0
fooRefl a b | Refl <- unsafeCoerce Refl :: Foo a b :~: Char = pure Foo1
|]
stuffhave3 = [d| data Peano = Z | S Peano
type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano n = S (ToPeano (n-1))
type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
|]
witnesses [d| data Peano = Z | S Peano
type family ToPeano (n :: Nat) :: Peano where ToPeano 0 = Z; ToPeano n = S (ToPeano (n-1))
type family FromPeano (p :: Peano) :: Nat where FromPeano Z = 0; FromPeano (S n) = 1 + FromPeano n
|]
deriving instance Show (ToPeanoRefl n)
deriving instance Show (FromPeanoRefl p)
witnesses [d| type family Unspell (w :: Symbol) = (r :: Nat) | r -> w where
Unspell "zero" = 0
Unspell "one" = 1
Unspell "two" = 2
Unspell "three" = 3
|]
deriving instance Show (UnspellRefl w)
main = runQ (witnesses stuffhave2) >>= print
test@Just{} = reify_Elim (typeRep @Integer) (typeOf ((+1)::Integer->Integer))
lemma :: v -> TypeRep f -> TypeRep v
-> Maybe (TypeRep (v `Elim` f), f -> v `Elim` f)
lemma w f v = do d `Fun'` c <- pure f
witness <- v `reify_Elim` f
case witness of
Elim0 -> pure (c, ($ w))
Elim1 -> do (e, g) <- lemma w c v
pure (d `Fun` e, (g.))
data Tag = Source | Destination | CheckSource Bool | CheckDest Bool | Cut Bool
newtype TaggedAction (t :: Tag) = Tagged (IO ())
data Action where
Action :: Typeable t ⇒ TaggedAction t → Action
Catalyst :: Typeable (c → d) ⇒ (c → d) → Action
pattern A :: forall k a. () => forall b. (TaggedAction b ~~ a) => TypeRep b → TypeRep a
pattern A b ← (eqTypeRep (typeRep @TaggedAction) → Just HRefl) `App` b
reaction :: Action → Action → Maybe Action
reaction (Catalyst f) (Action v) = do (rep, f') ← lemma v (typeOf f) (typeOf v)
pure $ case rep of
_ `Fun'` _ → withTypeable rep (Catalyst $ f' f)
A indx → withTypeable indx (Action $ f' f)
member :: Eq a => a -> [a] -> Bool
member = elem
y $$ x = ($ y).($ x)
--Just (t3r, (($ elem) -> t3)) = lemma 'j' (typeOf $ member @Char) (typeOf 'j') -- https://ghc.haskell.org/trac/ghc/ticket/14293
Just (t3r, (($ "joe").($ elem) -> t3@True)) = lemma 'j' (typeOf $ member @Char) (typeOf 'j')
Just (t4r, (($ 'o').($ elem) -> t4@True)) = lemma "joe" (typeOf $ member @Char) (typeOf "joe")
-- Just (t4'r, ('x' $$ elem -> t4'@False)) = lemma "joe" (typeOf $ member @Char) (typeOf "joe") -- Same bug
Just (t4'r, (($ 'x').($ elem) -> t4'@False)) = lemma "joe" (typeOf $ member @Char) (typeOf "joe")
t0@Nothing = lemma "joe" (typeOf ord) (typeOf "joe")
Just u0 = reify_FromPeano (typeRep @Z)
Just u1 = reify_FromPeano (typeRep @(S Z))
Just u2 = reify_FromPeano (typeRep @(S (S Z)))
Just un0 = reify_Unspell (typeRep @"zero")
Just un1 = reify_Unspell (typeRep @"one")
Just un2 = reify_Unspell (typeRep @"two")
|
