Skip to content

Conversation

@datvo06
Copy link

@datvo06 datvo06 commented Dec 4, 2025

Closes #361

@datvo06 datvo06 changed the base branch from master to staging-llm December 4, 2025 16:23
Copy link
Contributor

@jfeser jfeser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This doesn't really address #361, which is about checking the type-correctness of the function. A solution to #361 needs to run some type checker (e.g. mypy).

I think a type checker based version would be both simpler and more robust.

@datvo06
Copy link
Author

datvo06 commented Dec 4, 2025

@jfeser Thanks! I see, so we directly do the static analysis. Is the expected solution somewhere along this line?

import tempfile
from mypy import api

def _type_check_code(self, code: str, expected_type: type) -> None:
    """Run mypy on generated code to verify type correctness."""
    # Write code to temp file for mypy
    with tempfile.NamedTemporaryFile(mode='w', suffix='.py', delete=False) as f:
        f.write(code)
        temp_path = f.name
    
    try:
        result = api.run([temp_path, '--no-error-summary', '--no-pretty'])
        stdout, stderr, exit_code = result
        
        if exit_code != 0:
            raise SynthesisError(f"Type check failed:\n{stdout}", code)
    finally:
        import os
        os.unlink(temp_path)

@jfeser
Copy link
Contributor

jfeser commented Dec 4, 2025

I suspect the hard part of #361 will be giving the type checker appropriate context so that it can check code that uses types not defined by the LLM. E.g.

class User:
    name: str
    age: int
    salary: float

@Template.define
def _validation() -> Callable[[User], bool]:
    '''Write a function to check that users named Jack make at least $200000'''
    ...

The type checker needs to see the definition of User.

@datvo06
Copy link
Author

datvo06 commented Dec 4, 2025

@jfeser I see, thanks! I think I got a better idea now. Let me try another iteration.
Additionally, I think the synthesis handler would also need to quote the type, maybe recursively to the context of generation?

@datvo06
Copy link
Author

datvo06 commented Dec 4, 2025

@jfeser I made another attempt in #422

@eb8680 eb8680 added blocked and removed blocked labels Dec 11, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

effectful.handlers.llm.synthesis should type-check generated code

4 participants