TypeApplications does not imply AllowAmbiguousTypes
[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
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 PtrRepLifted' :: TyCon 'PtrRepLifted
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 PtrRepLifted' PtrRepLifted' = 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 TypeRepX allows you to specify an arbitrary
133 -- constraint on the inner TypeRep
134 data TypeRepX :: (forall k. k -> Constraint) -> Type where
135 TypeRepX :: forall k (c :: forall k'. k' -> Constraint) (a :: k).
136 c a => TypeRep a -> TypeRepX 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 (TypeRepX ConstTrue) where
143 show (TypeRepX tr) = show tr
144
145 -- can't write Show (TypeRepX c) because c's kind mentions a forall,
146 -- and the impredicativity check gets nervous. See #11519
147 instance Show (TypeRepX IsType) where
148 show (TypeRepX tr) = show tr
149
150 -- Just enough functionality to get through example. No parentheses
151 -- or other niceties.
152 instance Read (TypeRepX 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 -> [TypeRepX ConstTrue]
160 read_token "String" = return (TypeRepX $ typeRep @String)
161 read_token other = do
162 (TyConX tc, _) <- readsPrec p other
163 return (TypeRepX (TyCon tc))
164
165 mk_app :: TypeRepX ConstTrue -> TypeRepX ConstTrue -> TypeRepX ConstTrue
166 mk_app (TypeRepX f) (TypeRepX a) = case kindRep f of
167 TyCon Arrow `TyApp` k1 `TyApp` _
168 | Just HRefl <- k1 `eqT` kindRep a -> TypeRepX (TyApp f a)
169 _ -> error "ill-kinded type"
170
171 -- instance Read (TypeRepX ((~~) Type)) RAE: need (~~) :: forall k1. k1 -> forall k2. k2 -> Constraint
172 -- RAE: need kind signatures on classes
173
174 -- TypeRepX ((~~) 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 (TypeRepX IsType) where
182 readsPrec p s = case readsPrec @(TypeRepX ConstTrue) p s of
183 [(TypeRepX tr, "")]
184 | Just HRefl <- eqT (kindRep tr) (typeRep @Type)
185 -> [(TypeRepX 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 'PtrRepLifted where tyCon = PtrRepLifted'
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, TypeRepX 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, TypeRepX IsType)]
390 -> (forall (s :: TSchema). Schema s -> IO a)
391 -> IO a
392 go [] thing = thing Nil
393 go ((name, TypeRepX 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