gistfile1.txt

module LE where
  
  -- These are the core types used in LE projects
  
  data Entity end
  
  data Background (e : Entity) end
  
  data Nonexistant (e : Entity) end
  
  data family Predicate end
  
  data family Relation end
  
  data Pred (p : Predicate) (e : Entity) end
  
  data Rel (r : Relation) (e x : Entity) end
  
  data instance Relation where
    | Exp : Relation
    | Subj : Relation
  end
  
  
  
  
  
  -- These are some utility types that make things easier
  
  let exists : (Entity -> Type) -> Type where
    | exists p = Rec { witness : Entity, proof : p witness }
  end
  
  let and : Type -> Type -> Type where
    | and p q = Rec { fst : p, snd : q }
  end
  
  
  
  
  
  -- Categories are syntactic types. They can be interpreted into Golem types.
  
  data family Category end
  
  let family interpCat (c : Category) : Type end
  
  data instance Category where
    | Expression : Category
  end
  
  let instance interpCat where
    | interpCat Expression = Quoted Type
  end
  
  
  
  -- A rule type is a function over categories. They can be interpreted into
  -- Golem types.
  
  data RuleType where
    | RDone (c : Category) : RuleType
    | RArg (c : Category) (r : RuleType) : RuleType
  end
  
  let interpRule : RuleType -> Type where
    | interpRule (RDone c) = interpCat c
    | interpRule (RArg c r) = interpCat c -> interpRule r
  end
  
  
  
  -- A qrule type is a prenex quantified rule type. They can be interpreted
  -- into Golem types.
  
  data QRuleType where
    | QRDone (r : RuleType) : QRuleType
    | QRForall (a : Type) (f : a -> QRuleType) : QRuleType
  end
  
  let interpQRule : QRuleType -> Type where
    | interpQRule (QRDone r) = interpRule r
    | interpQRule (QRForall a f) = {x : a} -> interpQRule (f x)
  end
  
  
  
  -- A word is a triple of a form string, a category, and an inhabitant of the
  -- category's interpretation.
  
  data Word where
    | MkWord (w : Rec { form : String
                      , category : Category
                      , meaning : interpCat category
                      })
        : Word
  end
  
  
  
  -- A rule is a pair of a qrule type, and an inhabitant of it's
  -- interpretation.
  
  data Rule where
    | MkRule (r : Rec { ruleType : QRuleType
                      , ruleMeaning : interpQRule ruleType
                      })
             : Rule
  end
  
  
  
  
  
  reset qr from Entity to Type end
  
  -- This is a demo of categories and interpretation thereof.
  
  data instance Category where
    | EXP : Category
    | S : Category
    | NP : Category
    | D : Category
    | N : Category
    | VP : Category
  end
  
  let instance interpCat where
    | interpCat EXP = Quoted Type
    | interpCat S = Quoted[qr] (Entity -> Type)
    | interpCat NP = Quoted[qr] Entity
    | interpCat D = Quoted[qr] (Entity -> Type) -> Quoted[qr] Entity
    | interpCat N = Quoted[qr] (Entity -> Type)
    | interpCat VP = Quoted[qr] (Entity -> Entity -> Type)
  end
  
  
  
  
  
  
  -- This is a demo of defining rules. There's going to be some syntactic
  -- sugar for this, so that this rule can be written with
  --   ruleType = NP -o VP -o S
  
  let r : Rule where
    | r = MkRule
          { ruleType = QRDone (RArg NP (RArg VP (RDone S)))
          , ruleMeaning = \x f -> `(~f ~x)
          }
  end
  
  let r2 : Rule where
    | r2 = MkRule
           { ruleType = QRDone (RArg D (RArg N (RDone NP)))
           , ruleMeaning = \f x -> f x
           }
  end
  
  let r3 : Rule where
    | r3 = MkRule
           { ruleType = QRDone (RArg S (RDone EXP))
           , ruleMeaning = \p -> `(reset qr in exists (\e -> ~p e))
           }
  end
  
  
  
  
  
  
  -- This is a demo of defining predicates.
  
  data instance Predicate where
    | Bark : Predicate
    | Dog : Predicate
  end
  
  
  
  
  
  -- This is a demo of defining words.
  
  let a : Word where
    | a =
       MkWord
       { form = "a"
       , category = D
       , meaning = \p -> `(shift qr in exists (\x -> and (~p x) (continue x)))
       }
  end
  
  let dog : Word where
    | dog =
       MkWord
       { form = "dog"
       , category = N
       , meaning = `(\x -> Pred Dog x)
       }
  end
  
  let it : Word where
    | it =
        MkWord
        { form = "it"
        , category = NP
        , meaning = `(require x : Entity in x)
        }
  end
  
  let barked : Word where
    | barked =
        MkWord
        { form = "barked"
        , category = VP
        , meaning = `(\x e -> and (Pred Bark e)
                                  (Rel Subj e x))
        }
  end

end