disco 0.1.0.0 → 0.1.1.0

raw patch · 18 files changed

+218/−62 lines, 18 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• CHANGELOG.md +8/−0
• README.md +40/−0
• disco.cabal +3/−3
• example/truthtable.disco +19/−0
• lib/string.disco +7/−0
• src/Disco/Error.hs +3/−0
• src/Disco/Interactive/Commands.hs +35/−5
• src/Disco/Syntax/Operators.hs +3/−3
• src/Disco/Syntax/Prims.hs +8/−5
• src/Disco/Typecheck/Solve.hs +65/−33
• src/Disco/Typecheck/Util.hs +1/−2
• src/Disco/Types.hs +2/−0
• test/logic-bools/expected +6/−0
• test/logic-bools/input +10/−4
• test/repl-doc/expected +1/−1
• test/repl-help/expected +1/−0
• test/repl-proptest/expected +2/−2
• test/types-standalone-ops/expected +4/−4

@@ -0,0 +1,8 @@+* 0.1.1.0 (21 January 2022)++  - `->`, `/\`, `\/` syntax for implies, and, or+  - `truthtable.disco` example+  - Coinductively check user-defined types for qualifiers (#317)+  - Additional documentation++* 0.1.0.0 (17 January 2022): initial release

@@ -20,7 +20,32 @@   (if you don't know what that is, then you don't have it), see the   [instructions here](https://www.haskell.org/ghcup/install/) for a   PowerShell command to run.+    - If you use PowerShell, note that after running the magic+      PowerShell command to set up `ghcup`, you need to close and+      reopen PowerShell in order for it to recognize the `cabal`+      command.++- Run `cabal update`, which will download the latest information about+  Haskell packages.+ - Now run `cabal install disco` at a command prompt.++    - Note that this may take a very long time, on the order of an+      hour or so.+    - The good news is that most of this work only needs to be done+      once, even if you later install an updated version of disco.+      Even if installation fails partway through, the work already+      completed up to that point need not be redone.+    - On OSX, if building fails with an error like `ghc: could not+      execute: opt`, it means you need to install LLVM.  The easiest+      way to do this is to first [follow the instructions to install+      Homebrew](https://brew.sh/) (if you don't already have it), and+      then type++          brew install llvm++      at a terminal prompt.+ - If it works, you should be able to now type `disco` at a command   prompt, which should display a message like this: @@ -31,6 +56,21 @@      Disco>     ```++- If installation seems like it succeeded but the `disco` command is+  not recognized, it may be an issue with your path environment+  variable settings.  Try running `disco` using an explicit path:+    - `~/.cabal/bin/disco` on Linux or OSX+    - `C:\cabal\bin\disco` on Windows+    - If those don't work, poke around and see if you can figure+      out where the `cabal/bin` folder is on your computer, and+      run `disco` from there.+    - If you wish, you may add the `cabal/bin` folder (wherever it is+      located) to your `Path` (Windows) or `PATH` (Linux/OSX)+      environment variable, so that you can run disco simply by typing+      `disco`.  However, this step is optional.++  If you encounter any difficulties, please let me know --- either come talk to me or [open a GitHub

@@ -1,6 +1,6 @@ cabal-version:       2.4 name:                disco-version:             0.1.0.0+version:             0.1.1.0 synopsis:            Functional programming language for teaching discrete math. description:         Disco is a simple functional programming language for use in                      teaching discrete math.  Its syntax is designed to be close@@ -9,7 +9,7 @@ license-file:        LICENSE author:              Disco team maintainer:          byorgey@gmail.com-copyright:           Disco team 2016 (see LICENSE)+copyright:           Disco team 2016-2022 (see LICENSE) category:            Language  tested-with:         GHC == 8.10.4@@ -18,7 +18,7 @@  data-files:          *.disco -extra-source-files:  README.md, stack.yaml, example/*.disco, repl/*.hs+extra-source-files:  README.md, CHANGELOG.md, stack.yaml, example/*.disco, repl/*.hs                      docs/tutorial/example/*.disco                      --- TEST FILES BEGIN (updated automatically by add-test-files.hs) ---                      test/README.md

@@ -0,0 +1,19 @@+import string++||| Print a truth table for a binary boolean operation.  Intended to be used with+||| the :print command, as in+|||+|||   :print truthtable(~/\~)+!!! truthtable(~/\~) == "| F | F | F |\n| F | T | F |\n| T | F | F |\n| T | T | T |"+truthtable : (Bool * Bool -> Bool) -> List(Char)+truthtable(op) =+  unlines [ fmtrow [x,y,op(x,y)] | x <- enumerate(Bool), y <- enumerate(Bool) ]++||| Format a row of Boolean values with intervening | characters.+!!! fmtrow [true, false, false, true] == "| T | F | F | T |"+fmtrow : List(Bool) -> List(Char)+fmtrow(bs) = append("|", concat([ append(fmtbool(b), " |") | b <- bs ]))++fmtbool : Bool -> List(Char)+fmtbool(true) = " T"+fmtbool(false) = " F"

@@ -0,0 +1,7 @@+-- type String = List(Char)++unlines : List(List(Char)) -> List(Char)+unlines([]) = []+unlines([l]) = l+unlines(l :: ls) = append(l, append("\n", unlines(ls)))+

@@ -108,6 +108,9 @@ rtd :: String -> Sem r Doc rtd page = "https://disco-lang.readthedocs.io/en/latest/reference/" <> text page <> ".html" +issue :: Int -> Sem r Doc+issue n = "See https://github.com/disco-lang/disco/issues/" <> text (show n)+ cyclicImportError   :: Members '[Reader PA, LFresh] r   => [ModuleName] -> Sem r Doc

@@ -1,4 +1,5 @@ {-# LANGUAGE OverloadedStrings  #-}+{-# LANGUAGE PatternSynonyms    #-} {-# LANGUAGE StandaloneDeriving #-}  -----------------------------------------------------------------------------@@ -71,7 +72,7 @@                                                    toPrim) import           Disco.Typecheck import           Disco.Typecheck.Erase-import           Disco.Types                      (toPolyType)+import           Disco.Types                      (pattern TyString, toPolyType) import           Disco.Value  ------------------------------------------------------------@@ -87,6 +88,7 @@   ShowDefn  :: Name Term -> REPLExpr 'CShowDefn  -- Show a variable's definition   Parse     :: Term      -> REPLExpr 'CParse     -- Show the parsed AST   Pretty    :: Term      -> REPLExpr 'CPretty    -- Pretty-print a term+  Print     :: Term      -> REPLExpr 'CPrint     -- Print a string   Ann       :: Term      -> REPLExpr 'CAnn       -- Show type-annotated term   Desugar   :: Term      -> REPLExpr 'CDesugar   -- Show a desugared term   Compile   :: Term      -> REPLExpr 'CCompile   -- Show a compiled term@@ -130,6 +132,7 @@   | CShowDefn   | CParse   | CPretty+  | CPrint   | CAnn   | CDesugar   | CCompile@@ -208,6 +211,7 @@     SomeCmd nopCmd,     SomeCmd parseCmd,     SomeCmd prettyCmd,+    SomeCmd printCmd,     SomeCmd reloadCmd,     SomeCmd showDefnCmd,     SomeCmd typeCheckCmd,@@ -441,16 +445,17 @@ handleEval (Eval m) = do   mi <- inputToState @TopInfo $ loadParsedDiscoModule False FromCwdOrStdlib REPLModule m   addToREPLModule mi-  forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm . fst)+  forM_ (mi ^. miTerms) (mapError EvalErr . evalTerm True . fst)   -- garbageCollect? -evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => ATerm -> Sem r Value-evalTerm at = do+-- First argument = should the value be printed?+evalTerm :: Members (Error EvalError ': State TopInfo ': Output Message ': EvalEffects) r => Bool -> ATerm -> Sem r Value+evalTerm pr at = do   env <- use @TopInfo topEnv   v <- runInputConst env $ eval (compileTerm at)    tydefs <- use @TopInfo (replModInfo . to allTydefs)-  info $ runInputConst tydefs $ prettyValue' ty v+  when pr $ info $ runInputConst tydefs $ prettyValue' ty v    modify @TopInfo $     (replModInfo . miTys %~ Ctx.insert (QName (QualifiedName REPLModule) (string2Name "it")) (toPolyType ty)) .@@ -655,6 +660,31 @@  handlePretty :: Members '[LFresh, Output Message] r => REPLExpr 'CPretty -> Sem r () handlePretty (Pretty t) = info $ pretty' t++------------------------------------------------------------+-- :print++printCmd :: REPLCommand 'CPrint+printCmd =+  REPLCommand+    { name = "print",+      helpcmd = ":print <expr>",+      shortHelp = "Print a string without the double quotes, interpreting special characters",+      category = User,+      cmdtype = ColonCmd,+      action = \x -> handlePrint x,+      parser = Print <$> term+    }++handlePrint :: Members (Error DiscoError ': State TopInfo ': Output Message ': EvalEffects) r => REPLExpr 'CPrint -> Sem r ()+handlePrint (Print t) = do+  (at, _) <- inputToState . typecheckTop $ inferTop t+  let ty = getType at+  case ty of+    TyString -> do+      v <- mapError EvalErr . evalTerm False $ at+      info $ text (vlist vchar v)+    _        -> err $ "Argument to :print must have type List(Char), not" <+> pretty' ty  ------------------------------------------------------------ -- :reload

@@ -165,11 +165,11 @@     , bopInfo InL  Subset  ["subset", "⊆"]     , bopInfo InL  Elem    ["elem", "∈"]     ]-  , [ bopInfo InR  And     ["and", "∧", "&&"]+  , [ bopInfo InR  And     ["/\\", "and", "∧", "&&"]     ]-  , [ bopInfo InR  Or      ["or", "∨", "||"]+  , [ bopInfo InR  Or      ["\\/", "or", "∨", "||"]     ]-  , [ bopInfo InR Impl     ["==>", "implies"]+  , [ bopInfo InR Impl     ["->", "==>", "implies"]     ]   ]   where

@@ -195,10 +195,10 @@   , PrimFloor    ==> "floor(x) is the largest integer which is <= x."   , PrimCeil     ==> "ceiling(x) is the smallest integer which is >= x."   , PrimAbs      ==> "abs(x) is the absolute value of x.  Also written |x|."-  , PrimUOp Not  ==> "Logical negation: ¬true = false and ¬false = true.  Also written 'not'."-  , PrimBOp And  ==> "Logical conjunction (and): true and true = true; otherwise x and y = false."-  , PrimBOp Or   ==> "Logical disjunction (or): false or false = false; otherwise x or y = true."-  , PrimBOp Impl ==> "Logical implication (implies): true ==> false = false; otherwise x ==> y = true."+  , PrimUOp Not  ==> "Logical negation: not(true) = false and not(false) = true."+  , PrimBOp And  ==> "Logical conjunction (and): true /\\ true = true; otherwise x /\\ y = false."+  , PrimBOp Or   ==> "Logical disjunction (or): false \\/ false = false; otherwise x \\/ y = true."+  , PrimBOp Impl ==> "Logical implication (implies): true -> false = false; otherwise x -> y = true."   , PrimBOp Eq   ==> "Equality test.  x == y is true if x and y are equal."   , PrimBOp Neq  ==> "Inequality test.  x /= y is true if x and y are unequal."   , PrimBOp Lt   ==> "Less-than test. x < y is true if x is less than (but not equal to) y."@@ -225,5 +225,8 @@   , PrimFloor    ==> "round"   , PrimCeil     ==> "round"   , PrimAbs      ==> "abs"-  , PrimUOp Not  ==> "not"+  , PrimUOp Not  ==> "logic-ops"+  , PrimBOp And  ==> "logic-ops"+  , PrimBOp Or   ==> "logic-ops"+  , PrimBOp Impl ==> "logic-ops"   ]

@@ -43,6 +43,7 @@ import           Disco.Effects.State import           Polysemy import           Polysemy.Error+import           Polysemy.Input import           Polysemy.Output  import           Disco.Messages@@ -230,9 +231,9 @@ -- Top-level solver algorithm  solveConstraint-  :: Members '[Fresh, Error SolveError, Output Message] r-  => TyDefCtx -> Constraint -> Sem r S-solveConstraint tyDefns c = do+  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r+  => Constraint -> Sem r S+solveConstraint c = do    -- Step 1. Open foralls (instantiating with skolem variables) and   -- collect wanted qualifiers; also expand disjunctions.  Result in a@@ -249,16 +250,18 @@    -- Now try continuing with each set and pick the first one that has   -- a solution.-  asum' (map (uncurry (solveConstraintChoice tyDefns)) qcList)+  asum' (map (uncurry solveConstraintChoice) qcList)  solveConstraintChoice-  :: Members '[Fresh, Error SolveError, Output Message] r-  => TyDefCtx -> TyVarInfoMap -> [SimpleConstraint] -> Sem r S-solveConstraintChoice tyDefns quals cs = do+  :: Members '[Fresh, Error SolveError, Output Message, Input TyDefCtx] r+  => TyVarInfoMap -> [SimpleConstraint] -> Sem r S+solveConstraintChoice quals cs = do    debugPretty quals   debug $ vcat (map pretty' cs) +  tyDefns <- input @TyDefCtx+   -- Step 2. Check for weak unification to ensure termination. (a la   -- Traytel et al). @@ -273,7 +276,7 @@   debug "------------------------------"   debug "Running simplifier..." -  (vm, atoms, theta_simp) <- simplify tyDefns quals cs+  (vm, atoms, theta_simp) <- simplify quals cs   debug "Done running simplifier. Results:"    debugPretty vm@@ -306,7 +309,7 @@   debug "------------------------------"   debug "Checking WCCs for skolems..." -  (g', theta_skolem) <- checkSkolems tyDefns vm g+  (g', theta_skolem) <- checkSkolems vm g   debugPretty theta_skolem    -- We don't need to ensure that theta_skolem respects sorts since@@ -372,7 +375,7 @@ -- Step 1. Constraint decomposition.  decomposeConstraint-  :: Members '[Fresh, Error SolveError] r+  :: Members '[Fresh, Error SolveError, Input TyDefCtx] r   => Constraint -> Sem r [(TyVarInfoMap, [SimpleConstraint])] decomposeConstraint (CSub t1 t2) = return [(mempty, [t1 :<: t2])] decomposeConstraint (CEq  t1 t2) = return [(mempty, [t1 :=: t2])]@@ -391,16 +394,37 @@ decomposeConstraint (COr cs)     = concat <$> filterErrors (map decomposeConstraint cs)  decomposeQual-  :: Members '[Fresh, Error SolveError] r+  :: Members '[Fresh, Error SolveError, Input TyDefCtx] r   => Type -> Qualifier -> Sem r TyVarInfoMap-decomposeQual (TyAtom a) q             = checkQual q a-  -- XXX Really we should be able to check by induction whether a-  -- user-defined type has a certain sort.-decomposeQual ty@(TyCon (CUser _) _) q = throw $ Unqual q ty-decomposeQual ty@(TyCon c tys) q-  = case qualRules c q of+decomposeQual = go S.empty+  where+    go :: Members '[Fresh, Error SolveError, Input TyDefCtx] r+       => Set (String, [Type], Qualifier) -> Type -> Qualifier -> Sem r TyVarInfoMap++    -- For a type atom, call out to checkQual.+    go _ (TyAtom a) q = checkQual q a++    -- Coinductively check user-defined types for a qualifier.  Keep+    -- track of a set of user-defined types and qualifiers we have+    -- seen.  Every time we encounter a new one, add it to the set and+    -- recurse on its unfolding.  If we ever encounter one we have+    -- already seen, we can assume by coinduction that the qualifier+    -- is satisfied.+    go seen (TyCon (CUser t) tys) q = do+      case (t, tys, q) `S.member` seen of+        True -> return mempty+        False -> do+          tyDefns <- input @TyDefCtx+          case M.lookup t tyDefns of+            Nothing  -> error $ show t ++ " not in ty defn map!!"+            Just (TyDefBody _ body) -> do+              let ty' = body tys+              go (S.insert (t, tys, q) seen) ty' q++    -- Otherwise, decompose a type constructor according to the qualRules.+    go seen ty@(TyCon c tys) q = case qualRules c q of       Nothing -> throw $ Unqual q ty-      Just qs -> mconcat <$> zipWithM (maybe (return mempty) . decomposeQual) tys qs+      Just qs -> mconcat <$> zipWithM (maybe (return mempty) . go seen) tys qs  checkQual   :: Members '[Fresh, Error SolveError] r@@ -427,9 +451,9 @@ --   (b <: v), where v is a type variable and b is a base type.  simplify-  :: Members '[Error SolveError, Output Message] r-  => TyDefCtx -> TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)-simplify tyDefns origVM cs+  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r+  => TyVarInfoMap -> [SimpleConstraint] -> Sem r (TyVarInfoMap, [(Atom, Atom)], S)+simplify origVM cs   = (\(SS vm' cs' s' _) -> (vm', map extractAtoms cs', s'))   -- contFreshMT :: Monad m => FreshMT m a -> Integer -> m a   -- "Run a FreshMT computation given a starting index for fresh name generation."@@ -456,7 +480,7 @@     -- Iterate picking one simplifiable constraint and simplifying it     -- until none are left.     simplify'-      :: Members '[State SimplifyState, Fresh, Error SolveError, Output Message] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Output Message, Input TyDefCtx] r       => Sem r ()     simplify' = do       -- q <- gets fst@@ -517,7 +541,7 @@     -- has already been seen before (due to expansion of a recursive     -- type), just throw it away and stop.     simplifyOne-      :: Members '[State SimplifyState, Fresh, Error SolveError] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r       => SimpleConstraint -> Sem r ()     simplifyOne c = do       seen <- use ssSeen@@ -528,14 +552,15 @@           simplifyOne' c      simplifyOne'-      :: Members '[State SimplifyState, Fresh, Error SolveError] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r       => SimpleConstraint -> Sem r ()      -- If we have an equality constraint, run unification on it.  The     -- resulting substitution is applied to the remaining constraints     -- as well as prepended to the current substitution. -    simplifyOne' (ty1 :=: ty2) =+    simplifyOne' (ty1 :=: ty2) = do+      tyDefns <- input @TyDefCtx       case unify tyDefns [(ty1, ty2)] of         Nothing -> throw NoUnify         Just s' -> extendSubst s'@@ -549,7 +574,8 @@       = simplifyOne' (ty1 :=: ty2)      -- Otherwise, expand the user-defined type and continue.-    simplifyOne' (TyCon (CUser t) ts :<: ty2) =+    simplifyOne' (TyCon (CUser t) ts :<: ty2) = do+      tyDefns <- input @TyDefCtx       case M.lookup t tyDefns of         Nothing  -> error $ show t ++ " not in ty defn map!"         Just (TyDefBody _ body) ->@@ -559,7 +585,8 @@     simplifyOne' (ty1@TyVar{} :<: ty2@(TyCon (CUser _) _))       = simplifyOne' (ty1 :=: ty2) -    simplifyOne' (ty1 :<: TyCon (CUser t) ts) =+    simplifyOne' (ty1 :<: TyCon (CUser t) ts) = do+      tyDefns <- input @TyDefCtx       case M.lookup t tyDefns of         Nothing  -> error $ show t ++ " not in ty defn map!"         Just (TyDefBody _ body) ->@@ -604,7 +631,7 @@       error $ "Impossible! simplifyOne' " ++ show s ++ " :<: " ++ show t      expandStruct-      :: Members '[State SimplifyState, Fresh, Error SolveError] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r       => Name Type -> Con -> SimpleConstraint -> Sem r ()     expandStruct a c con = do       as <- mapM (const (TyVar <$> fresh (string2Name "a"))) (arity c)@@ -616,7 +643,7 @@     -- 2. apply s' to constraints     -- 3. apply s' to qualifier map and decompose     extendSubst-      :: Members '[State SimplifyState, Fresh, Error SolveError] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r       => S -> Sem r ()     extendSubst s' = do       ssSubst %= (s'@@)@@ -624,7 +651,7 @@       substVarMap s'      substVarMap-      :: Members '[State SimplifyState, Fresh, Error SolveError] r+      :: Members '[State SimplifyState, Fresh, Error SolveError, Input TyDefCtx] r       => S -> Sem r ()     substVarMap s' = do       vm <- use ssVarMap@@ -688,9 +715,9 @@ --   only unsorted variables, just unify them all with the skolem and --   remove those components. checkSkolems-  :: Members '[Error SolveError, Output Message] r-  => TyDefCtx -> TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)-checkSkolems tyDefns vm graph = do+  :: Members '[Error SolveError, Output Message, Input TyDefCtx] r+  => TyVarInfoMap -> Graph Atom -> Sem r (Graph UAtom, S)+checkSkolems vm graph = do   let skolemWCCs :: [Set Atom]       skolemWCCs = filter (any isSkolem) $ G.wcc graph @@ -715,9 +742,14 @@     noSkolems (AVar (U v)) = UV v     noSkolems (AVar (S v)) = error $ "Skolem " ++ show v ++ " remaining in noSkolems" +    unifyWCCs+      :: Members '[Error SolveError, Output Message, Input TyDefCtx] r+      => Graph Atom -> S -> [Set Atom] -> Sem r (Graph UAtom, S)     unifyWCCs g s []     = return (G.map noSkolems g, s)     unifyWCCs g s (u:us) = do       debug $ "Unifying" <+> pretty' (u:us) <> "..."++      tyDefns <- input @TyDefCtx        let g' = foldl' (flip G.delete) g u 

@@ -113,8 +113,7 @@   => Sem (Writer Constraint ': r) a -> Sem r (a, S) solve m = do   (a, c) <- withConstraint m-  tds <- ask @TyDefCtx-  res <- runSolve . solveConstraint tds $ c+  res <- runSolve . inputToReader . solveConstraint $ c   case res of     Left e  -> throw (Unsolvable e)     Right s -> return (a, s)

@@ -667,6 +667,8 @@  -- XXX coinductively check whether user-defined types are searchable --   e.g.  L = Unit + N * L  ought to be searchable.+--   See https://github.com/disco-lang/disco/issues/318.+ -- | Decide whether a type is searchable, i.e. effectively enumerable. isSearchable :: Type -> Bool isSearchable TyProp         = False

@@ -7,12 +7,18 @@ false false false+false true true true false true+true false+true+true+false+true true true false

@@ -7,14 +7,20 @@ false and true false and false true && false+true /\ false true or true true or false false or true false or false true || false+true \/ false not true not false-true ==> true -true ==> false -false ==> true -false ==> false +true ==> true+true ==> false+false ==> true+false ==> false+true -> true+true -> false+false -> true+false -> false

@@ -30,7 +30,7 @@ Alternative syntax: ¬~ precedence level 15 -Logical negation: ¬true = false and ¬false = true.  Also written 'not'.+Logical negation: not(true) = false and not(false) = true.  https://disco-lang.readthedocs.io/en/latest/reference/not.html 

@@ -6,6 +6,7 @@ :help             Show help :load <filename>  Load a file :names            Show all names in current scope+:print <expr>     Print a string without the double quotes, interpreting special characters :reload           Reloads the most recently loaded file :test <property>  Test a property using random examples 

@@ -1,10 +1,10 @@   - Test passed: not false   - Test passed: {1, 2} =!= {2, 1}-  - Test passed: ∃a, b. (a and b) =!= (a or b)+  - Test passed: ∃a, b. (a /\ b) =!= (a \/ b)     Found example:       a = false       b = false-  - Test result mismatch for: ∀a, b. (a and b) =!= (a or b)+  - Test result mismatch for: ∀a, b. (a /\ b) =!= (a \/ b)     - Left side:  true     - Right side: false     Counterexample:

@@ -1,4 +1,4 @@-~and~ : Bool × Bool → Bool-false and true : Bool-λx. x and true : Bool → Bool-let f : (Bool × Bool → Bool) → Bool = λg. g(true, false) in f(~and~) : Bool+~/\~ : Bool × Bool → Bool+false /\ true : Bool+λx. x /\ true : Bool → Bool+let f : (Bool × Bool → Bool) → Bool = λg. g(true, false) in f(~/\~) : Bool