480db090c3da1fec90649cfa5b96e2128d081b2a
[ghc.git] / testsuite / tests / dependent / should_compile / RaeJobTalk.hs
1 {- Copyright (c) 2016 Richard Eisenberg
2 -}
3
4 {-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications, AllowAmbiguousTypes,
5 ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
6 TypeInType, ConstraintKinds, UndecidableInstances,
7 FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
8 FlexibleContexts, StandaloneDeriving, InstanceSigs,
9 RankNTypes, UndecidableSuperClasses #-}
10
11 module RaeJobTalk where
12
13 import Data.Type.Bool
14 import Data.Type.Equality hiding ((:~~:)(..))
15 import GHC.TypeLits
16 import Data.Proxy
17 import GHC.Exts
18 import Data.Kind
19 import Unsafe.Coerce
20 import Data.Char
21 import Data.Maybe
22
23 -------------------------------
24 -- Utilities
25
26 -- Heterogeneous propositional equality
27 data (a :: k1) :~~: (b :: k2) where
28 HRefl :: a :~~: a
29
30 -- Type-level inequality
31 type a /= b = Not (a == b)
32
33 -- append type-level lists (schemas)
34 type family s1 ++ s2 where
35 '[] ++ s2 = s2
36 (s ': s1) ++ s2 = s ': (s1 ++ s2)
37
38 -- This is needed in order to prove disjointness, because GHC can't
39 -- handle inequality well.
40 assumeEquality :: forall a b r. ((a ~ b) => r) -> r
41 assumeEquality thing = case unsafeCoerce Refl :: a :~: b of
42 Refl -> thing
43
44 -- Shorter name for shorter example
45 eq :: TestEquality f => f a -> f b -> Maybe (a :~: b)
46 eq = testEquality
47
48 -------------------------------
49 -- Singleton lists
50
51 -- Unlike in the singletons paper, we now have injective type
52 -- families, so we use that to model singletons; it's a bit
53 -- cleaner than the original approach
54 type family Sing = (r :: k -> Type) | r -> k
55
56 -- Cute type synonym.
57 type Π = Sing
58
59 -- Really, just singleton lists. Named Schema for better output
60 -- during example.
61 data Schema :: forall k. [k] -> Type where
62 Nil :: Schema '[]
63 (:>>) :: Sing h -> Schema t -> Schema (h ': t)
64 infixr 5 :>>
65 type instance Sing = Schema
66
67 -- Append singleton lists
68 (%:++) :: Schema a -> Schema b -> Schema (a ++ b)
69 Nil %:++ x = x
70 (a :>> b) %:++ c = a :>> (b %:++ c)
71
72 --------------------------------
73 -- Type-indexed type representations
74 -- Based on "A reflection on types"
75
76 data TyCon (a :: k) where
77 Int :: TyCon Int
78 Bool :: TyCon Bool
79 Char :: TyCon Char
80 List :: TyCon []
81 Maybe :: TyCon Maybe
82 Arrow :: TyCon (->)
83 TYPE :: TyCon TYPE
84 RuntimeRep :: TyCon RuntimeRep
85 LiftedRep' :: TyCon 'LiftedRep
86 -- If extending, add to eqTyCon too
87
88 eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
89 eqTyCon Int Int = Just HRefl
90 eqTyCon Bool Bool = Just HRefl
91 eqTyCon Char Char = Just HRefl
92 eqTyCon List List = Just HRefl
93 eqTyCon Maybe Maybe = Just HRefl
94 eqTyCon Arrow Arrow = Just HRefl
95 eqTyCon TYPE TYPE = Just HRefl
96 eqTyCon RuntimeRep RuntimeRep = Just HRefl
97 eqTyCon LiftedRep' LiftedRep' = Just HRefl
98 eqTyCon _ _ = Nothing
99
100 -- Check whether or not a type is really a plain old tycon;
101 -- necessary to avoid warning in kindRep
102 type family Primitive (a :: k) :: Constraint where
103 Primitive (_ _) = ('False ~ 'True)
104 Primitive _ = (() :: Constraint)
105
106 data TypeRep (a :: k) where
107 TyCon :: forall (a :: k). (Primitive a, Typeable k) => TyCon a -> TypeRep a
108 TyApp :: TypeRep a -> TypeRep b -> TypeRep (a b)
109
110 -- Equality on TypeReps
111 eqT :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
112 eqT (TyCon tc1) (TyCon tc2) = eqTyCon tc1 tc2
113 eqT (TyApp f1 a1) (TyApp f2 a2) = do
114 HRefl <- eqT f1 f2
115 HRefl <- eqT a1 a2
116 return HRefl
117 eqT _ _ = Nothing
118
119
120 --------------------------------------
121 -- Existentials
122
123 data TyConX where
124 TyConX :: forall (a :: k). (Primitive a, Typeable k) => TyCon a -> TyConX
125
126 instance Read TyConX where
127 readsPrec _ "Int" = [(TyConX Int, "")]
128 readsPrec _ "Bool" = [(TyConX Bool, "")]
129 readsPrec _ "List" = [(TyConX List, "")]
130 readsPrec _ _ = []
131
132 -- This variant of SomeTypeRep allows you to specify an arbitrary
133 -- constraint on the inner TypeRep
134 data SomeTypeRep :: (forall k. k -> Constraint) -> Type where
135 SomeTypeRep :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
136 c a => TypeRep a -> SomeTypeRep c
137
138 -- This constraint is always satisfied
139 class ConstTrue (a :: k) -- needs the :: k to make it a specified tyvar
140 instance ConstTrue a
141
142 instance Show (SomeTypeRep ConstTrue) where
143 show (SomeTypeRep tr) = show tr
144
145 -- can't write Show (SomeTypeRep c) because c's kind mentions a forall,
146 -- and the impredicativity check gets nervous. See #11519
147 instance Show (SomeTypeRep IsType) where
148 show (SomeTypeRep tr) = show tr
149
150 -- Just enough functionality to get through example. No parentheses
151 -- or other niceties.
152 instance Read (SomeTypeRep ConstTrue) where
153 readsPrec p s = do
154 let tokens = words s
155 tyreps <- mapM read_token tokens
156 return (foldl1 mk_app tyreps, "")
157
158 where
159 read_token :: String -> [SomeTypeRep ConstTrue]
160 read_token "String" = return (SomeTypeRep $ typeRep @String)
161 read_token other = do
162 (TyConX tc, _) <- readsPrec p other
163 return (SomeTypeRep (TyCon tc))
164
165 mk_app :: SomeTypeRep ConstTrue -> SomeTypeRep ConstTrue -> SomeTypeRep ConstTrue
166 mk_app (SomeTypeRep f) (SomeTypeRep a) = case kindRep f of
167 TyCon Arrow `TyApp` k1 `TyApp` _
168 | Just HRefl <- k1 `eqT` kindRep a -> SomeTypeRep (TyApp f a)
169 _ -> error "ill-kinded type"
170
171 -- instance Read (SomeTypeRep ((~~) Type)) RAE: need (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
172 -- RAE: need kind signatures on classes
173
174 -- SomeTypeRep ((~~) Type)
175 -- (~~) :: forall k1 k2. k1 -> k2 -> Constraint
176 -- I need: (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
177
178 class k ~~ Type => IsType (x :: k)
179 instance k ~~ Type => IsType (x :: k)
180
181 instance Read (SomeTypeRep IsType) where
182 readsPrec p s = case readsPrec @(SomeTypeRep ConstTrue) p s of
183 [(SomeTypeRep tr, "")]
184 | Just HRefl <- eqT (kindRep tr) (typeRep @Type)
185 -> [(SomeTypeRep tr, "")]
186 _ -> error "wrong kind"
187
188 -----------------------------
189 -- Get the kind of a type
190
191 kindRep :: TypeRep (a :: k) -> TypeRep k
192 kindRep (TyCon _) = typeRep
193 kindRep (TyApp (f :: TypeRep (tf :: k1 -> k)) _) = case kindRep f :: TypeRep (k1 -> k) of
194 TyApp _ res -> res
195
196 -- Convert an explicit TypeRep into an implicit one. Doesn't require unsafeCoerce
197 -- in Core
198 withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
199 withTypeable tr thing = unsafeCoerce (Don'tInstantiate thing :: DI a r) tr
200 newtype DI a r = Don'tInstantiate (Typeable a => r)
201
202 -----------------------------
203 -- Implicit TypeReps (Typeable)
204
205 class (Primitive a, Typeable k) => TyConAble (a :: k) where
206 tyCon :: TyCon a
207
208 instance TyConAble Int where tyCon = Int
209 instance TyConAble Bool where tyCon = Bool
210 instance TyConAble Char where tyCon = Char
211 instance TyConAble [] where tyCon = List
212 instance TyConAble Maybe where tyCon = Maybe
213 instance TyConAble (->) where tyCon = Arrow
214 instance TyConAble TYPE where tyCon = TYPE
215 instance TyConAble 'LiftedRep where tyCon = LiftedRep'
216 instance TyConAble RuntimeRep where tyCon = RuntimeRep
217
218 -- Can't just define Typeable the way we want, because the instances
219 -- overlap. So we have to mock up instance chains via closed type families.
220 class Typeable' a (b :: Bool) where
221 typeRep' :: TypeRep a
222
223 type family CheckPrim a where
224 CheckPrim (_ _) = 'False
225 CheckPrim _ = 'True
226
227 -- NB: We need the ::k and the ::Constraint so that this has a CUSK, allowing
228 -- the polymorphic recursion with TypeRep. See also #9200, though the requirement
229 -- for the constraints is correct.
230 type Typeable (a :: k) = (Typeable' a (CheckPrim a) :: Constraint)
231
232 instance TyConAble a => Typeable' a 'True where
233 typeRep' = TyCon tyCon
234
235 instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
236 typeRep' = TyApp typeRep typeRep
237
238 typeRep :: forall a. Typeable a => TypeRep a
239 typeRep = typeRep' @_ @(CheckPrim a)
240
241 -----------------------------
242 -- Useful instances
243
244 instance Show (TypeRep a) where
245 show (TyCon tc) = show tc
246 show (TyApp tr1 tr2) = show tr1 ++ " " ++ show tr2
247
248 deriving instance Show (TyCon a)
249
250 instance TestEquality TypeRep where
251 testEquality tr1 tr2
252 | Just HRefl <- eqT tr1 tr2
253 = Just Refl
254 | otherwise
255 = Nothing
256
257 ---------------------------
258 -- More singletons
259
260 -- a TypeRep really is a singleton
261 type instance Sing = (TypeRep :: Type -> Type)
262
263 data SSymbol :: Symbol -> Type where
264 SSym :: KnownSymbol s => SSymbol s
265 type instance Sing = SSymbol
266
267 instance TestEquality SSymbol where
268 testEquality :: forall s1 s2. SSymbol s1 -> SSymbol s2 -> Maybe (s1 :~: s2)
269 testEquality SSym SSym = sameSymbol @s1 @s2 Proxy Proxy
270
271 instance Show (SSymbol name) where
272 show s@SSym = symbolVal s
273
274
275 --------------
276 -- Finds Read and Show instances for the example
277 getReadShowInstances :: TypeRep a
278 -> ((Show a, Read a) => r)
279 -> r
280 getReadShowInstances tr thing
281 | Just HRefl <- eqT tr (typeRep @Int) = thing
282 | Just HRefl <- eqT tr (typeRep @Bool) = thing
283 | Just HRefl <- eqT tr (typeRep @Char) = thing
284
285 | TyApp list_rep elt_rep <- tr
286 , Just HRefl <- eqT list_rep (typeRep @[])
287 = getReadShowInstances elt_rep $ thing
288
289 | otherwise = error $ "I don't know how to read or show " ++ show tr
290
291 -------------------------
292 -- A named column in our database
293 data Column = Attr Symbol Type
294 type Col = 'Attr
295
296 -- Singleton for columns
297 data SColumn :: Column -> Type where
298 Col :: Sing s -> TypeRep ty -> SColumn (Col s ty)
299 type instance Sing = SColumn
300
301 -- Extract the type of a column
302 type family ColType col where
303 ColType (Col _ ty) = ty
304
305 -- A schema is an ordered list of named attributes
306 type TSchema = [Column]
307
308 -- predicate to check that a schema is free of a certain attribute
309 type family ColNotIn name s where
310 ColNotIn _ '[] = 'True
311 ColNotIn name ((Col name' _) ': t) =
312 (name /= name') && (ColNotIn name t)
313
314 -- predicate to check that two schemas are disjoint
315 type family Disjoint s1 s2 where
316 Disjoint '[] _ = 'True
317 Disjoint ((Col name ty) ': t) s = (ColNotIn name s) && (Disjoint t s)
318
319 -- A Row is one row of our database table, keyed by its schema.
320 data Row :: TSchema -> Type where
321 EmptyRow :: Row '[]
322 (::>) :: ColType col -> Row s -> Row (col ': s)
323 infixr 5 ::>
324
325 -- Map a predicate over all the types in a schema
326 type family AllSchemaTys c sch where
327 AllSchemaTys _ '[] = (() :: Constraint)
328 AllSchemaTys c (col ': cols) = (c (ColType col), AllSchemaTys c cols)
329
330 -- Convenient abbreviations for being to print and parse the types
331 -- in a schema
332 type ShowSchema s = AllSchemaTys Show s
333 type ReadSchema s = AllSchemaTys Read s
334
335 -- We can easily print out rows, as long as the data are printable
336 instance ShowSchema s => Show (Row s) where
337 show EmptyRow = ""
338 show (h ::> t) = show h ++ " " ++ show t
339
340 -- In our simplistic case, we just store the list of rows. A more
341 -- sophisticated implementation could store some identifier to the connection
342 -- to an external database.
343 data Table :: TSchema -> Type where
344 Table :: [Row s] -> Table s
345
346 instance ShowSchema s => Show (Table s) where
347 show (Table rows) = unlines (map show rows)
348
349 -- The following functions parse our very simple flat file database format.
350
351 -- The file, with a name ending in ".table", consists of a sequence of lines,
352 -- where each line contains one entry in the table. There is no row separator;
353 -- if a row contains n pieces of data, that row is represented in n lines in
354 -- the file.
355
356 -- A schema is stored in a file ending in ".schema".
357 -- Each line is a column name followed by its type.
358
359 -- Read a row of a table
360 readRow :: ReadSchema s => Schema s -> [String] -> (Row s, [String])
361 readRow Nil strs = (EmptyRow, strs)
362 readRow (_ :>> _) [] = error "Ran out of data while processing row"
363 readRow (_ :>> schTail) (sh:st) = (read sh ::> rowTail, strTail)
364 where (rowTail, strTail) = readRow schTail st
365
366 -- Read in a table
367 readRows :: ReadSchema s => Schema s -> [String] -> [Row s]
368 readRows _ [] = []
369 readRows sch lst = (row : tail)
370 where (row, strTail) = readRow sch lst
371 tail = readRows sch strTail
372
373 -- Read in one line of a .schema file. Note that the type read must have kind *
374 readCol :: String -> (String, SomeTypeRep IsType)
375 readCol str = case break isSpace str of
376 (name, ' ' : ty) -> (name, read ty)
377 _ -> schemaError $ "Bad parse of " ++ str
378
379 -- Load in a schema.
380 withSchema :: String
381 -> (forall (s :: TSchema). Schema s -> IO a)
382 -> IO a
383 withSchema filename thing_inside = do
384 schString <- readFile filename
385 let schEntries = lines schString
386 cols = map readCol schEntries
387 go cols thing_inside
388 where
389 go :: [(String, SomeTypeRep IsType)]
390 -> (forall (s :: TSchema). Schema s -> IO a)
391 -> IO a
392 go [] thing = thing Nil
393 go ((name, SomeTypeRep tr) : cols) thing
394 = go cols $ \schema ->
395 case someSymbolVal name of
396 SomeSymbol (_ :: Proxy name) ->
397 thing (Col (SSym @name) tr :>> schema)
398
399 -- Load in a table of a given schema
400 loadTable :: ReadSchema s => String -> Schema s -> IO (Table s)
401 loadTable name schema = do
402 dataString <- readFile name
403 return (Table $ readRows schema (lines dataString))
404
405 -- In order to define strongly-typed projection from a row, we need to have a notion
406 -- that one schema is a subset of another. We permit the schemas to have their columns
407 -- in different orders. We define this subset relation via two inductively defined
408 -- propositions. In Haskell, these inductively defined propositions take the form of
409 -- GADTs. In their original form, they would look like this:
410 {-
411 data InProof :: Column -> Schema -> * where
412 InHere :: InProof col (col ': schTail)
413 InThere :: InProof col cols -> InProof col (a ': cols)
414
415 data SubsetProof :: Schema -> Schema -> * where
416 SubsetEmpty :: SubsetProof '[] s'
417 SubsetCons :: InProof col s' -> SubsetProof cols s'
418 -> SubsetProof (col ': cols) s'
419 -}
420 -- However, it would be convenient to users of the database library not to require
421 -- building these proofs manually. So, we define type classes so that the compiler
422 -- builds the proofs automatically. To make everything work well together, we also
423 -- make the parameters to the proof GADT constructors implicit -- i.e. in the form
424 -- of type class constraints.
425
426 data InProof :: Column -> TSchema -> Type where
427 InHere :: InProof col (col ': schTail)
428 InThere :: In name u cols => InProof (Col name u) (a ': cols)
429
430 class In (name :: Symbol) (u :: Type) (sch :: TSchema) where
431 inProof :: InProof (Col name u) sch
432
433 -- These instances must be INCOHERENT because they overlap badly. The coherence
434 -- derives from the fact that one schema will mention a name only once, but this
435 -- is beyond our capabilities to easily encode, given the lack of a solver for
436 -- type-level finite maps.
437 instance {-# INCOHERENT #-} In name u ((Col name u) ': schTail) where
438 inProof = InHere
439 instance {-# INCOHERENT #-} In name u cols => In name u (a ': cols) where
440 inProof = InThere
441
442 data SubsetProof :: TSchema -> TSchema -> Type where
443 SubsetEmpty :: SubsetProof '[] s'
444 SubsetCons :: (In name u s', Subset cols s')
445 => Proxy name -> Proxy u -> SubsetProof ((Col name u) ': cols) s'
446
447 class SubsetSupport s s' => Subset (s :: TSchema) (s' :: TSchema) where
448 subset :: SubsetProof s s'
449
450 -- The use of this constraint family allows us to assume a subset relationship
451 -- when we recur on the structure of s.
452 type SubsetSupport s s' :: Constraint
453
454 instance Subset '[] s' where
455 subset = SubsetEmpty
456 type SubsetSupport '[] s' = ()
457
458 instance (In name u s', Subset cols s') =>
459 Subset ((Col name u) ': cols) s' where
460 subset = SubsetCons Proxy Proxy
461 type SubsetSupport ((Col name u) ': cols) s' = Subset cols s'
462
463 -- To access the data in a structured (and well-typed!) way, we use
464 -- an RA (short for Relational Algebra). An RA is indexed by the schema
465 -- of the data it produces.
466
467 data RA :: TSchema -> Type where
468 -- The RA includes all data represented by the handle.
469 Read :: Table s -> RA s
470
471 -- The RA is a Cartesian product of the two RAs provided. Note that
472 -- the schemas of the two provided RAs must be disjoint.
473 Product :: (Disjoint s s' ~ 'True) => RA s -> RA s' -> RA (s ++ s')
474
475 -- The RA is a projection conforming to the schema provided. The
476 -- type-checker ensures that this schema is a subset of the data
477 -- included in the provided RA.
478 Project :: Subset s' s => RA s -> RA s'
479
480 -- The RA contains only those rows of the provided RA for which
481 -- the provided expression evaluates to True. Note that the
482 -- schema of the provided RA and the resultant RA are the same
483 -- because the columns of data are the same. Also note that
484 -- the expression must return a Bool for this to type-check.
485 Select :: Expr s Bool -> RA s -> RA s
486
487 -- Other constructors would be added in a more robust database
488 -- implementation.
489
490 -- An Expr is used with the Select constructor to choose some
491 -- subset of rows from a table. Expressions are indexed by the
492 -- schema over which they operate and the return value they
493 -- produce.
494 data Expr :: TSchema -> Type -> Type where
495 (:+), (:-), (:*), (:/) :: Expr s Int -> Expr s Int -> Expr s Int
496
497 (:<), (:<=), (:>), (:>=), (:==), (:/=)
498 :: Ord a => Expr s a -> Expr s a -> Expr s Bool
499
500 -- A literal
501 Literal :: ty -> Expr s ty
502
503 -- element of a list
504 ElementOf :: Eq ty => Expr s ty -> Expr s [ty] -> Expr s Bool
505
506 -- Projection in an expression -- evaluates to the value
507 -- of the named column.
508 Element :: In name ty s => Proxy name -> Expr s ty
509
510 -- Choose the elements of one list based on truth values in another
511 choose :: [Bool] -> [a] -> [a]
512 choose bs as = [ a | (a,True) <- zip as bs ]
513
514 -- Project a component of one row, assuming that the desired projection
515 -- is valid.
516 projectRow :: forall sub super.
517 Subset sub super => Row super -> Row sub
518 projectRow r = case subset @sub @super of
519 SubsetEmpty -> EmptyRow
520 SubsetCons (_ :: Proxy name) (_ :: Proxy ty) ->
521 find_datum inProof r ::> projectRow r
522 where
523 find_datum :: InProof (Col name ty) s -> Row s -> ty
524 find_datum InHere (h ::> _) = h
525 find_datum InThere (_ ::> t) = find_datum inProof t
526
527 -- Evaluate an Expr
528 eval :: Expr s ty -> Row s -> ty
529 eval (a :+ b) r = eval a r + eval b r
530 eval (a :- b) r = eval a r - eval b r
531 eval (a :* b) r = eval a r * eval b r
532 eval (a :/ b) r = eval a r `div` eval b r
533 eval (a :< b) r = eval a r < eval b r
534 eval (a :<= b) r = eval a r <= eval b r
535 eval (a :> b) r = eval a r > eval b r
536 eval (a :>= b) r = eval a r >= eval b r
537 eval (a :== b) r = eval a r == eval b r
538 eval (a :/= b) r = eval a r /= eval b r
539 eval (Literal n) _ = n
540 eval (ElementOf elt list) r = eval elt r `elem` eval list r
541 eval (Element (_ :: Proxy name)) r = get_element inProof r
542 where
543 get_element :: InProof (Col name ty) s -> Row s -> ty
544 get_element InHere (elt ::> _) = elt
545 get_element InThere (_ ::> tail) = get_element inProof tail
546
547 -- Append two rows. Needed for Cartesian product.
548 rowAppend :: Row s -> Row s' -> Row (s ++ s')
549 rowAppend EmptyRow r = r
550 rowAppend (h ::> t) r = h ::> rowAppend t r
551
552 -- The query function is the eliminator for an RA. It returns a list of
553 -- rows containing the data produced by the RA. In the IO monad only
554 -- because more sophisticated implementations would actually go out to
555 -- a DB server for this.
556 query :: RA s -> IO [Row s]
557 query (Read (Table rows)) = return rows
558 query (Product ra rb) = do
559 rowsa <- query ra
560 rowsb <- query rb
561 return [ rowAppend rowa rowb | rowa <- rowsa, rowb <- rowsb ]
562 query (Project ra) = map projectRow <$> query ra
563 query (Select expr ra) = filter (eval expr) <$> query ra
564
565 field :: forall name ty s. In name ty s => Expr s ty
566 field = Element (Proxy :: Proxy name)
567
568
569
570
571
572
573
574
575 -- A schema is a list of columns, with
576 -- data Column = Col String Type
577 -- NB: Dependent type support is still experimental
578 checkIn :: Π name -> Π ty -> Π schema
579 -> (In name ty schema => r)
580 -> r
581 checkIn name _ Nil _
582 = schemaError ("Field " ++ show name ++ " not found.")
583 checkIn name ty ((Col name' ty') :>> rest) callback
584 = case (name `eq` name', ty `eq` ty') of
585 (Just Refl, Just Refl) -> callback
586 (Just _, _) -> schemaError ("Found " ++ show name ++
587 " but it maps to " ++ show ty')
588 _ -> checkIn name ty rest callback
589
590 -- example call:
591 -- checkIn "id" Int schema ({- access "id" and assume it has type Int -})
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608 -- Establish a Subset constraint
609 checkSubset :: Π sch1 -> Π sch2 -> (Subset sch1 sch2 => r) -> r
610 checkSubset Nil _ callback = callback
611 checkSubset (Col name ty :>> rest) super callback
612 = checkSubset rest super $
613 checkIn name ty super $
614 callback
615
616 -- Check that two names are distinct
617 checkNotEqual :: forall (name1 :: Symbol) name2 r.
618 Π name1 -> Π name2
619 -> (((name1 /= name2) ~ 'True) => r) -> r
620 checkNotEqual name1 name2 callback
621 = case name1 `eq` name2 of
622 Just Refl -> schemaError $ "Found " ++ show name1 ++
623 " in both supposedly disjoint schemas."
624 Nothing -> assumeEquality @(name1 /= name2) @'True $
625 callback
626
627 -- Establish a ColNotIn condition
628 checkColNotIn :: Π name -> Π sch2
629 -> ((ColNotIn name sch2 ~ 'True) => r) -> r
630 checkColNotIn _ Nil callback = callback
631 checkColNotIn name (Col name' _ :>> rest) callback
632 = checkNotEqual name name' $
633 checkColNotIn name rest $
634 callback
635
636 -- Establish a Disjointness constraint
637 checkDisjoint :: Π sch1 -> Π sch2
638 -> ((Disjoint sch1 sch2 ~ 'True) => r) -> r
639 checkDisjoint Nil _ callback = callback
640 checkDisjoint (Col name _ :>> rest) sch2 callback
641 = checkColNotIn name sch2 $
642 checkDisjoint rest sch2 $
643 callback
644
645 -- Establish a ShowSchema constraint
646 checkShowSchema :: Π sch -> (ShowSchema sch => r) -> r
647 checkShowSchema Nil callback = callback
648 checkShowSchema (Col _ ty :>> rest) callback
649 = getReadShowInstances ty $
650 checkShowSchema rest $
651 callback
652
653 -- Establish a ReadSchema constraint
654 checkReadSchema :: Π sch -> (ReadSchema sch => r) -> r
655 checkReadSchema Nil callback = callback
656 checkReadSchema (Col _ ty :>> rest) callback
657 = getReadShowInstances ty $
658 checkReadSchema rest $
659 callback
660
661 -- Terminate program with an easy-to-understand message
662 schemaError :: String -> a
663 schemaError str = errorWithoutStackTrace $ "Schema validation error: " ++ str
664
665 -------------------------
666 type NameSchema = [ Col "first" String, Col "last" String ]
667
668 printName :: Row NameSchema -> IO ()
669 printName (first ::> last ::> _) = putStrLn (first ++ " " ++ last)
670
671 readDB classes_sch students_sch = do
672 classes_tab <- loadTable "classes.table" classes_sch
673 students_tab <- loadTable "students.table" students_sch
674
675 putStr "Whose students do you want to see? "
676 prof <- getLine
677
678 let joined = Project (
679 Select (field @"id" @Int `ElementOf` field @"students") (
680 Product (Select (field @"prof" :== Literal prof) (Read classes_tab))
681 (Read students_tab)))
682 rows <- query joined
683 mapM_ printName rows
684
685 ------------------
686 main :: IO ()
687 main = withSchema "classes.schema" $ \classes_sch ->
688 withSchema "students.schema" $ \students_sch ->
689 checkDisjoint classes_sch students_sch $
690 checkIn (SSym @"students") (typeRep @[Int]) (classes_sch %:++ students_sch) $
691 checkIn (SSym @"prof") (typeRep @String) classes_sch $
692 checkIn (SSym @"last") (typeRep @String) (classes_sch %:++ students_sch) $
693 checkIn (SSym @"id") (typeRep @Int) (classes_sch %:++ students_sch) $
694 checkIn (SSym @"first") (typeRep @String) (classes_sch %:++ students_sch) $
695 checkReadSchema students_sch $
696 checkReadSchema classes_sch $
697 readDB classes_sch students_sch