Ticket #11716: RaeJobTalk.hs

File RaeJobTalk.hs, 23.4 KB (added by goldfire, 4 years ago)
Line 
1{- Copyright (c) 2016 Richard Eisenberg
2 -}
3
4{-# LANGUAGE TypeOperators, TypeFamilies, TypeApplications,
5             ExplicitForAll, ScopedTypeVariables, GADTs, TypeFamilyDependencies,
6             TypeInType, ConstraintKinds, UndecidableInstances,
7             FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies,
8             FlexibleContexts, StandaloneDeriving, InstanceSigs,
9             RankNTypes, UndecidableSuperClasses #-}
10
11module RaeJobTalk where
12
13import Data.Type.Bool
14import Data.Type.Equality
15import GHC.TypeLits
16import Data.Proxy
17import GHC.Exts
18import Data.Kind
19import Unsafe.Coerce
20import Data.Char
21import Data.Maybe
22
23-------------------------------
24-- Utilities
25
26-- Heterogeneous propositional equality
27data (a :: k1) :~~: (b :: k2) where
28  HRefl :: a :~~: a
29
30-- Type-level inequality
31type a /= b = Not (a == b)
32
33-- append type-level lists (schemas)
34type 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.
40assumeEquality :: forall a b r. ((a ~ b) => r) -> r
41assumeEquality thing = case unsafeCoerce Refl :: a :~: b of
42  Refl -> thing
43
44-- Shorter name for shorter example
45eq :: TestEquality f => f a -> f b -> Maybe (a :~: b)
46eq = 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
54type family Sing = (r :: k -> Type) | r -> k
55
56-- Cute type synonym.
57type Π = Sing
58
59-- Really, just singleton lists. Named Schema for better output
60-- during example.
61data Schema :: forall k. [k] -> Type where
62  Nil :: Schema '[]
63  (:>>) :: Sing h -> Schema t -> Schema (h ': t)
64infixr 5 :>>
65type instance Sing = Schema
66
67-- Append singleton lists
68(%:++) :: Schema a -> Schema b -> Schema (a ++ b)
69Nil %:++ x = x
70(a :>> b) %:++ c = a :>> (b %:++ c)
71
72--------------------------------
73-- Type-indexed type representations
74-- Based on "A reflection on types"
75
76data 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
88eqTyCon :: TyCon a -> TyCon b -> Maybe (a :~~: b)
89eqTyCon Int Int = Just HRefl
90eqTyCon Bool Bool = Just HRefl
91eqTyCon Char Char = Just HRefl
92eqTyCon List List = Just HRefl
93eqTyCon Maybe Maybe = Just HRefl
94eqTyCon Arrow Arrow = Just HRefl
95eqTyCon TYPE TYPE = Just HRefl
96eqTyCon RuntimeRep RuntimeRep = Just HRefl
97eqTyCon PtrRepLifted' PtrRepLifted' = Just HRefl
98eqTyCon _ _ = Nothing
99
100-- Check whether or not a type is really a plain old tycon;
101-- necessary to avoid warning in kindRep
102type family Primitive (a :: k) :: Constraint where
103  Primitive (_ _) = ('False ~ 'True)
104  Primitive _     = (() :: Constraint)
105
106data 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
111eqT :: TypeRep a -> TypeRep b -> Maybe (a :~~: b)
112eqT (TyCon tc1) (TyCon tc2) = eqTyCon tc1 tc2
113eqT (TyApp f1 a1) (TyApp f2 a2) = do
114  HRefl <- eqT f1 f2
115  HRefl <- eqT a1 a2
116  return HRefl
117eqT _ _ = Nothing
118
119
120--------------------------------------
121-- Existentials
122
123data TyConX where
124  TyConX :: forall (a :: k). (Primitive a, Typeable k) => TyCon a -> TyConX
125
126instance 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
134data 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
139class ConstTrue (a :: k) -- needs the :: k to make it a specified tyvar
140instance ConstTrue a
141
142instance 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
147instance 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.
152instance 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
178class k ~~ Type => IsType (x :: k)
179instance k ~~ Type => IsType (x :: k)
180
181instance 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
191kindRep :: TypeRep (a :: k) -> TypeRep k
192kindRep (TyCon _) = typeRep
193kindRep (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
198withTypeable :: forall a r. TypeRep a -> (Typeable a => r) -> r
199withTypeable tr thing = unsafeCoerce (Don'tInstantiate thing :: DI a r) tr
200newtype DI a r = Don'tInstantiate (Typeable a => r)
201
202-----------------------------
203-- Implicit TypeReps (Typeable)
204
205class (Primitive a, Typeable k) => TyConAble (a :: k) where
206  tyCon :: TyCon a
207
208instance TyConAble Int       where tyCon = Int
209instance TyConAble Bool      where tyCon = Bool
210instance TyConAble Char      where tyCon = Char
211instance TyConAble []        where tyCon = List
212instance TyConAble Maybe     where tyCon = Maybe
213instance TyConAble (->)      where tyCon = Arrow
214instance TyConAble TYPE      where tyCon = TYPE
215instance TyConAble 'PtrRepLifted   where tyCon = PtrRepLifted'
216instance 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.
220class Typeable' (a :: k) (b :: Bool) where
221  typeRep' :: TypeRep a
222
223type 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.
230type Typeable (a :: k) = (Typeable' a (CheckPrim a) :: Constraint)
231
232instance TyConAble a => Typeable' a 'True where
233  typeRep' = TyCon tyCon
234
235instance (Typeable a, Typeable b) => Typeable' (a b) 'False where
236  typeRep' = TyApp typeRep typeRep
237
238typeRep :: forall a. Typeable a => TypeRep a
239typeRep = typeRep' @_ @_ @(CheckPrim a) -- RAE: #11512 says we need the extra @_.
240
241-----------------------------
242-- Useful instances
243
244instance Show (TypeRep a) where
245  show (TyCon tc) = show tc
246  show (TyApp tr1 tr2) = show tr1 ++ " " ++ show tr2
247
248deriving instance Show (TyCon a)
249
250instance 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
261type instance Sing = (TypeRep :: Type -> Type)
262
263data SSymbol :: Symbol -> Type where
264  SSym :: KnownSymbol s => SSymbol s
265type instance Sing = SSymbol
266
267instance 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
271instance Show (SSymbol name) where
272  show s@SSym = symbolVal s
273
274
275--------------
276-- Finds Read and Show instances for the example
277getReadShowInstances :: TypeRep a
278                     -> ((Show a, Read a) => r)
279                     -> r
280getReadShowInstances 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
293data Column = Attr Symbol Type
294type Col = 'Attr
295
296-- Singleton for columns
297data SColumn :: Column -> Type where
298  Col :: Sing s -> TypeRep ty -> SColumn (Col s ty)
299type instance Sing = SColumn
300
301-- Extract the type of a column
302type family ColType col where
303  ColType (Col _ ty) = ty
304
305-- A schema is an ordered list of named attributes
306type TSchema = [Column]
307
308-- predicate to check that a schema is free of a certain attribute
309type 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
315type 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.
320data Row :: TSchema -> Type where
321  EmptyRow :: Row '[]
322  (::>) :: ColType col -> Row s -> Row (col ': s)
323infixr 5 ::>
324
325-- Map a predicate over all the types in a schema
326type 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
332type ShowSchema s = AllSchemaTys Show s
333type ReadSchema s = AllSchemaTys Read s
334
335-- We can easily print out rows, as long as the data are printable
336instance 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.
343data Table :: TSchema -> Type where
344  Table :: [Row s] -> Table s
345
346instance 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
360readRow :: ReadSchema s => Schema s -> [String] -> (Row s, [String])
361readRow Nil             strs    = (EmptyRow, strs)
362readRow (_ :>> _)       []      = error "Ran out of data while processing row"
363readRow (_ :>> schTail) (sh:st) = (read sh ::> rowTail, strTail)
364  where (rowTail, strTail) = readRow schTail st
365
366-- Read in a table
367readRows :: ReadSchema s => Schema s -> [String] -> [Row s]
368readRows _   []  = []
369readRows 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 *
374readCol :: String -> (String, TypeRepX IsType)
375readCol str = case break isSpace str of
376  (name, ' ' : ty) -> (name, read ty)
377  _                -> schemaError $ "Bad parse of " ++ str
378
379-- Load in a schema.
380withSchema :: String
381           -> (forall (s :: TSchema). Schema s -> IO a)
382           -> IO a
383withSchema 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
400loadTable :: ReadSchema s => String -> Schema s -> IO (Table s)
401loadTable 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{-
411data InProof :: Column -> Schema -> * where
412  InHere  :: InProof col (col ': schTail)
413  InThere :: InProof col cols -> InProof col (a ': cols)
414
415data 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
426data InProof :: Column -> TSchema -> Type where
427  InHere  :: InProof col (col ': schTail)
428  InThere :: In name u cols => InProof (Col name u) (a ': cols)
429
430class 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.
437instance {-# INCOHERENT #-} In name u ((Col name u) ': schTail) where
438  inProof = InHere
439instance {-# INCOHERENT #-} In name u cols => In name u (a ': cols) where
440  inProof = InThere
441
442data 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
447class 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
454instance Subset '[] s' where
455  subset = SubsetEmpty
456  type SubsetSupport '[] s' = ()
457
458instance (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
467data 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.
494data 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
511choose :: [Bool] -> [a] -> [a]
512choose bs as = [ a | (a,True) <- zip as bs ]
513
514-- Project a component of one row, assuming that the desired projection
515-- is valid.
516projectRow :: forall sub super.
517              Subset sub super => Row super -> Row sub
518projectRow 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
528eval :: Expr s ty -> Row s -> ty
529eval (a :+ b)  r = eval a r +  eval b r
530eval (a :- b)  r = eval a r -  eval b r
531eval (a :* b)  r = eval a r *  eval b r
532eval (a :/ b)  r = eval a r `div` eval b r
533eval (a :< b)  r = eval a r <  eval b r
534eval (a :<= b) r = eval a r <= eval b r
535eval (a :> b)  r = eval a r >  eval b r
536eval (a :>= b) r = eval a r >= eval b r
537eval (a :== b) r = eval a r == eval b r
538eval (a :/= b) r = eval a r /= eval b r
539eval (Literal n)                 _ = n
540eval (ElementOf elt list)        r = eval elt r `elem` eval list r
541eval (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.
548rowAppend :: Row s -> Row s' -> Row (s ++ s')
549rowAppend EmptyRow  r = r
550rowAppend (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.
556query :: RA s -> IO [Row s]
557query (Read (Table rows)) = return rows
558query (Product ra rb) = do
559  rowsa <- query ra
560  rowsb <- query rb
561  return [ rowAppend rowa rowb | rowa <- rowsa, rowb <- rowsb ]
562query (Project ra)     = map projectRow <$> query ra
563query (Select expr ra) = filter (eval expr) <$> query ra
564
565field :: forall name ty s. In name ty s => Expr s ty
566field = 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
578checkIn :: Π name -> Π ty -> Π schema
579        -> (In name ty schema => r)
580        -> r
581checkIn name _  Nil                        _
582  = schemaError ("Field " ++ show name ++ " not found.")
583checkIn 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
609checkSubset :: Π sch1 -> Π sch2 -> (Subset sch1 sch2 => r) -> r
610checkSubset Nil                    _     callback = callback
611checkSubset (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
617checkNotEqual :: forall (name1 :: Symbol) name2 r.
618                 Π name1 -> Π name2
619              -> (((name1 /= name2) ~ 'True) => r) -> r
620checkNotEqual 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
628checkColNotIn :: Π name -> Π sch2
629              -> ((ColNotIn name sch2 ~ 'True) => r) -> r
630checkColNotIn _    Nil                    callback = callback
631checkColNotIn name (Col name' _ :>> rest) callback
632  = checkNotEqual name name' $
633    checkColNotIn name rest $
634    callback
635
636-- Establish a Disjointness constraint
637checkDisjoint :: Π sch1 -> Π sch2
638              -> ((Disjoint sch1 sch2 ~ 'True) => r) -> r
639checkDisjoint Nil                   _    callback = callback
640checkDisjoint (Col name _ :>> rest) sch2 callback
641  = checkColNotIn name sch2 $
642    checkDisjoint rest sch2 $
643    callback
644
645-- Establish a ShowSchema constraint
646checkShowSchema :: Π sch -> (ShowSchema sch => r) -> r
647checkShowSchema Nil                 callback = callback
648checkShowSchema (Col _ ty :>> rest) callback
649  = getReadShowInstances ty $
650    checkShowSchema rest $
651    callback
652
653-- Establish a ReadSchema constraint
654checkReadSchema :: Π sch -> (ReadSchema sch => r) -> r
655checkReadSchema Nil                 callback = callback
656checkReadSchema (Col _ ty :>> rest) callback
657  = getReadShowInstances ty $
658    checkReadSchema rest $
659    callback
660
661-- Terminate program with an easy-to-understand message
662schemaError :: String -> a
663schemaError str = errorWithoutStackTrace $ "Schema validation error: " ++ str
664
665-------------------------
666type NameSchema = [ Col "first" String, Col "last" String ]
667
668printName :: Row NameSchema -> IO ()
669printName (first ::> last ::> _) = putStrLn (first ++ " " ++ last)
670
671readDB 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------------------
686main :: IO ()
687main = 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