Skip to content

Commit

Permalink
Display multiple example types for things with nontrivial (non-parame…
Browse files Browse the repository at this point in the history
…tric) polymorphism (#388)

Closes #169.  Previously, we did this:
```
Disco> :type \x. x - 2
λx. x - 2 : ℤ → ℤ
```
However, this was a lie since in fact `\x. x - 2` is more general than that; but showing only one possible monomorphic type was still better than showing some generic monstrosity like `forall a. (N <: a, subtractive a) => a -> a`. 

Now, with this PR, we do this:
```
Disco> :type \x. x - 2
This expression has multiple possible types.  Some examples:
λx. x - 2 : ℤ → ℤ
λx. x - 2 : ℚ → ℚ
```
See #169 for more context and examples.

Briefly, in this PR, we:
- Change the solver to return a *list* of solution substitutions instead of just a single one
- Add a "solution limit" counter to the solver so it can stop early once it has hit the limit for the number of solutions we want.
    - In some cases (e.g. when checking a provided type) we just want one.
    - In other cases (when inferring a type) we set an arbitrary bound of 16.
    - This is not really ideal --- in theory we would want to use some kind of proper backtracking logic monad like `LogicT` but that seems difficult/impossible to incorporate into `polysemy` (https://stackoverflow.com/questions/62627695/running-the-nondet-effect-once-in-polysemy; polysemy-research/polysemy#246).
- "Thin" the resulting list of solutions by throwing away any solutions which are supertypes of another solution in the list.
- Add pretty-printing that distinguishes between a single solution and multiple solutions

It is still possible to make the solver blow up in case there are many possible container variables to instantiate.  *e.g.* expressions like `\x. \y. \z. \w. (set(x), set(y), set(z), set(w))` take a very long time to typecheck.  I have some ideas for how to improve this situation, but for now it's an uncommon corner case.
  • Loading branch information
byorgey authored Jun 5, 2024
1 parent b57e45b commit 10f21fb
Show file tree
Hide file tree
Showing 27 changed files with 545 additions and 245 deletions.
2 changes: 1 addition & 1 deletion build
Original file line number Diff line number Diff line change
@@ -1,2 +1,2 @@
#!/bin/sh
stack test --fast --file-watch --test-arguments '--hide-successes +RTS -N8 -RTS'
cabal test -j -O0
4 changes: 2 additions & 2 deletions feedback.yaml
Original file line number Diff line number Diff line change
@@ -1,3 +1,3 @@
loops:
test8: stack test --fast --test-arguments '--hide-successes +RTS -N8 -RTS'
test30: stack test --fast --test-arguments '--hide-successes +RTS -N30 -RTS'
build: cabal -j build -O0
test: cabal -j test -O0 --test-show-details=direct
27 changes: 1 addition & 26 deletions hie.yaml
Original file line number Diff line number Diff line change
@@ -1,27 +1,2 @@
cradle:
multi:
- path: "./explore"
config:
cradle:
none:
- path: "./nsf"
config:
cradle:
none:
- path: "./pubs"
config:
cradle:
none:
- path: "./notes"
config:
cradle:
none:
- path: "./example"
config:
cradle:
none:
- path: "./"
config:
cradle:
stack:
component: "disco:lib"
cabal:
3 changes: 2 additions & 1 deletion src/Disco/AST/Surface.hs
Original file line number Diff line number Diff line change
Expand Up @@ -632,7 +632,7 @@ containerDelims SetContainer = braces

prettyBranches :: Members '[Reader PA, LFresh] r => [Branch] -> Sem r (Doc ann)
prettyBranches = \case
[] -> error "Empty branches are disallowed."
[] -> text ""
b : bs ->
pretty b
$+$ foldr (($+$) . (text "," <+>) . pretty) empty bs
Expand Down Expand Up @@ -729,3 +729,4 @@ instance Pretty Pattern where
PFrac p1 p2 ->
withPA (getPA Div) $
lt (pretty p1) <+> text "/" <+> rt (pretty p2)
PNonlinear p _ -> pretty p
10 changes: 6 additions & 4 deletions src/Disco/Effects/Input.hs
Original file line number Diff line number Diff line change
@@ -1,7 +1,3 @@
-----------------------------------------------------------------------------

-----------------------------------------------------------------------------

-- |
-- Module : Disco.Effects.Input
-- Copyright : disco team and contributors
Expand All @@ -13,6 +9,7 @@
module Disco.Effects.Input (
module Polysemy.Input,
inputToState,
mapInput,
)
where

Expand All @@ -23,3 +20,8 @@ import Polysemy.State
-- | Run an input effect in terms of an ambient state effect.
inputToState :: forall s r a. Member (State s) r => Sem (Input s ': r) a -> Sem r a
inputToState = interpret (\case Input -> get @s)

-- | Use a function to (contravariantly) transform the input value in
-- an input effect.
mapInput :: forall s t r a. Member (Input s) r => (s -> t) -> Sem (Input t ': r) a -> Sem r a
mapInput f = interpret (\case Input -> inputs @s f)
32 changes: 22 additions & 10 deletions src/Disco/Interactive/Commands.hs
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE StandaloneDeriving #-}

Expand Down Expand Up @@ -33,8 +34,9 @@ import Data.Bifunctor (second)
import Data.Char (isSpace)
import Data.Coerce
import Data.List (find, isPrefixOf, sortBy, transpose)
import Data.List.NonEmpty qualified as NE
import Data.Map ((!))
import qualified Data.Map as M
import Data.Map qualified as M
import Data.Maybe (mapMaybe, maybeToList)
import Data.Typeable
import Disco.AST.Surface
Expand All @@ -43,6 +45,7 @@ import Disco.Compile
import Disco.Context as Ctx
import Disco.Desugar
import Disco.Doc
import Disco.Effects.Fresh (runFresh)
import Disco.Effects.Input
import Disco.Effects.LFresh
import Disco.Effects.State
Expand All @@ -66,7 +69,7 @@ import Disco.Parser (
withExts,
)
import Disco.Pretty hiding (empty, (<>))
import qualified Disco.Pretty as PP
import Disco.Pretty qualified as PP
import Disco.Property (prettyTestResult)
import Disco.Syntax.Operators
import Disco.Syntax.Prims (
Expand All @@ -84,8 +87,8 @@ import Polysemy.Output
import Polysemy.Reader
import System.FilePath (splitFileName)
import Text.Megaparsec hiding (State, runParser)
import qualified Text.Megaparsec.Char as C
import qualified Text.PrettyPrint.Boxes as B
import Text.Megaparsec.Char qualified as C
import Text.PrettyPrint.Boxes qualified as B
import Unbound.Generics.LocallyNameless (
Name,
name2String,
Expand Down Expand Up @@ -307,7 +310,7 @@ handleAnn ::
REPLExpr 'CAnn ->
Sem r ()
handleAnn (Ann t) = do
(at, _) <- typecheckTop $ inferTop t
(at, _) <- typecheckTop $ inferTop1 t
infoPretty at

------------------------------------------------------------
Expand All @@ -330,7 +333,7 @@ handleCompile ::
REPLExpr 'CCompile ->
Sem r ()
handleCompile (Compile t) = do
(at, _) <- typecheckTop $ inferTop t
(at, _) <- typecheckTop $ inferTop1 t
infoPretty . compileTerm $ at

------------------------------------------------------------
Expand All @@ -353,7 +356,7 @@ handleDesugar ::
REPLExpr 'CDesugar ->
Sem r ()
handleDesugar (Desugar t) = do
(at, _) <- typecheckTop $ inferTop t
(at, _) <- typecheckTop $ inferTop1 t
info $ pretty' . eraseDTerm . runDesugar . desugarTerm $ at

------------------------------------------------------------
Expand Down Expand Up @@ -802,7 +805,7 @@ tableCmd =

handleTable :: Members (Error DiscoError ': State TopInfo ': Output (Message ()) ': EvalEffects) r => REPLExpr 'CTable -> Sem r ()
handleTable (Table t) = do
(at, ty) <- inputToState . typecheckTop $ inferTop t
(at, ty) <- inputToState . typecheckTop $ inferTop1 t
v <- mapError EvalErr . evalTerm False $ at

tydefs <- use @TopInfo (replModInfo . to allTydefs)
Expand Down Expand Up @@ -1026,13 +1029,22 @@ typeCheckCmd =
, parser = TypeCheck <$> parseTermOrOp
}

maxInferredTypes :: Int
maxInferredTypes = 16

handleTypeCheck ::
Members '[Error DiscoError, Input TopInfo, LFresh, Output (Message ())] r =>
REPLExpr 'CTypeCheck ->
Sem r ()
handleTypeCheck (TypeCheck t) = do
(_, sig) <- typecheckTop $ inferTop t
info $ pretty' t <+> text ":" <+> pretty' sig
asigs <- typecheckTop $ inferTop maxInferredTypes t
sigs <- runFresh . mapInput (view (replModInfo . miTydefs)) $ thin $ NE.map snd asigs
let (toShow, extra) = NE.splitAt 8 sigs
when (length sigs > 1) $ info "This expression has multiple possible types. Some examples:"
info $
vcat $
map (\sig -> pretty' t <+> text ":" <+> pretty' sig) toShow
++ ["..." | not (P.null extra)]

------------------------------------------------------------

Expand Down
5 changes: 5 additions & 0 deletions src/Disco/Pretty.hs
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,8 @@ import Prelude hiding ((<>))

import Data.Bifunctor
import Data.Char (isAlpha)
import Data.List.NonEmpty (NonEmpty)
import qualified Data.List.NonEmpty as NE
import Data.Map (Map)
import qualified Data.Map as M
import Data.Ratio
Expand Down Expand Up @@ -93,6 +95,9 @@ pretty' = runReader initPA . runLFresh . pretty
instance Pretty a => Pretty [a] where
pretty = brackets . intercalate "," . map pretty

instance Pretty a => Pretty (NonEmpty a) where
pretty = pretty . NE.toList

instance (Pretty k, Pretty v) => Pretty (Map k v) where
pretty m = do
let es = map (\(k, v) -> pretty k <+> "->" <+> pretty v) (M.assocs m)
Expand Down
Loading

0 comments on commit 10f21fb

Please sign in to comment.