Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Typed Holes #779

Open
Heimdell opened this issue Aug 31, 2019 · 2 comments

Comments

@Heimdell
Copy link

commented Aug 31, 2019

Typed Holes

I propose we add a feature analoguous to haskell's TypedHoles with "there are these names in scope, and their inferred types". This is done by replacing some unwritten part if the program with _ token.

The existing way of approaching this problem in F# is putting a 1 or () in place of part of the program and seeing the compiler error. This, however, doesn't tell you what locally-defined names you can use and what their types are.

Pros and Cons

The advantages of making this adjustment to F# are:

  1. This feature will greatly improve implementations of any lens port of something type-heavy.

The disadvantages of making this adjustment to F# are

  1. The token "_" in expression context is lost to user.

Extra information

Estimated cost (XS, S, M, L, XL, XXL): M-L (type inference partial state dump might be inaccessible)

Affidavit (please submit!)

Please tick this by placing a cross in the box:

  • This is not a question (e.g. like one you might ask on stackoverflow) and I have searched stackoverflow for discussions of this issue
  • I have searched both open and closed suggestions on this site and believe this is not a duplicate
  • This is not something which has obviously "already been decided" in previous versions of F#. If you're questioning a fundamental design decision that has obviously already been taken (e.g. "Make F# untyped") then please don't submit it.

Please tick all that apply:

  • This is not a breaking change to the F# language design
  • I or my company would be willing to help implement and/or test this
@cartermp

This comment has been minimized.

Copy link
Member

commented Sep 3, 2019

For reference, here's an example of how a typed hole helps out in Haskell:

instance Functor (State s) where
  (<$>) :: (a -> b) -> State s a -> State s b
  f <$> State sa = State (\s-> let (a, s') = _ s in (f a, s'))
 -- Note the '_' on the previous line

Invoking with GHCi gives:

src/Course/State.hs:64:46: error:
    • Found hole: _ :: s -> (a1, b1)
      Where: ‘a1’, ‘b1’ are rigid type variables bound by
               the inferred types of
                 a :: a1
                 s' :: b1
               at src/Course/State.hs:64:36-48
             ‘s’ is a rigid type variable bound by
               the instance declaration
               at src/Course/State.hs:62:10-26
    • In the expression: _
      In the expression: _ s
      In a pattern binding: (a, s') = _ s
    • Relevant bindings include
        a :: a1 (bound at src/Course/State.hs:64:37)
        s' :: b1 (bound at src/Course/State.hs:64:40)
        s :: s (bound at src/Course/State.hs:64:28)
        sa :: s -> (a, s) (bound at src/Course/State.hs:64:15)
        f :: a -> b (bound at src/Course/State.hs:64:3)
        (<$>) :: (a -> b) -> State s a -> State s b
          (bound at src/Course/State.hs:64:5)
      Valid substitutions include
        undefined :: forall (a :: TYPE r).
                     GHC.Stack.Types.HasCallStack =>
                     a
          (imported qualified from ‘Prelude’ at src/Course/State.hs:9:1-29
           (and originally defined in ‘GHC.Err’))
   |
64 |   f <$> State sa = State (\s-> let (a, s') = _ s in (f a, s'))
   |                                              ^
Failed, 23 modules loaded.

And in this case, the sa value is correct, so the hole helped me out a lot. This is quite helpful for REPL-driven workflows, and you could imagine quick fixes in an IDE suggesting identifiers.

It's worth noting that there are also issues of ergonomics to consider. Sprinkling in a _ can be immensely helpful, but it can also lead to further confusion when the compiler generalizes things. Adjusting the previous example as such:

instance Functor (State s) where
  (<$>) :: (a -> b) -> State s a -> State s b
  f <$> State sa = State (\s -> let (a, s') = _ in (f a, s'))
-- Note the '_' now replaces the entire state function invocation

Gives:

src/Course/State.hs:64:47: error:
    • Found hole: _ :: (a1, b1)
      Where: ‘a1’, ‘b1’ are rigid type variables bound by
               the inferred types of
                 a :: a1
                 s' :: b1
               at src/Course/State.hs:64:37-47
    • In the expression: _
      In a pattern binding: (a, s') = _
      In the expression: let (a, s') = _ in (f a, s')
    • Relevant bindings include
        a :: a1 (bound at src/Course/State.hs:64:38)
        s' :: b1 (bound at src/Course/State.hs:64:41)
        s :: s (bound at src/Course/State.hs:64:28)
        sa :: s -> (a, s) (bound at src/Course/State.hs:64:15)
        f :: a -> b (bound at src/Course/State.hs:64:3)
        (<$>) :: (a -> b) -> State s a -> State s b
          (bound at src/Course/State.hs:64:5)
      Valid substitutions include
        undefined :: forall (a :: TYPE r).
                     GHC.Stack.Types.HasCallStack =>
                     a
          (imported qualified from ‘Prelude’ at src/Course/State.hs:9:1-29
           (and originally defined in ‘GHC.Err’))
   |
64 |   f <$> State sa = State (\s -> let (a, s') = _ in (f a, s'))
   |     

In this case, the intent being, "I know the structure of what I want but I just want to find the right types that represent how I produce that" can give something someone might find unexpected. This is another way to expose diagnostic limitations of the F# compiler, which could also help improving those limitations, but it could also just help make them more widespread.

@jindraivanek

This comment has been minimized.

Copy link

commented Sep 3, 2019

Type inference part can be done now with:

[<CompilerMessage("type hole", 9999)>]
let ___<'a> = failwith "type hole
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
3 participants
You can’t perform that action at this time.