Assistant

Experimental assistant for proving things. Not yet useful for anything.

Literally doesn’t work right now.

The main goal here is to find paths for converting between different types in Python. The approaches discussed in this answer implement the following techniques:

1. Exploring class hierarchy (subclass and superclass relationships) between types.
2. Using a unification-like approach to find common types and conversion paths between types.

Python is quite different from Lean, a theorem prover that finds paths between types for the purpose of proving mathematical statements. Because of it’s dynamic and less strict type system, we are instead trying to create dictionaries to hold and identify conversion functions for different pairs of types.

There are probably better/different approaches, this is just a proof of concept.

Triavial unification like-approach

I think this is closer to lean? 1. Define a set of conversion functions between different types. 2. Create a dictionary that maps pairs of types to their corresponding conversion functions. 3. Implement a unification function that takes two types and returns their common type, if one exists. 4. Implement a function that finds a conversion path between two expressions by unifying their types and using the conversion functions. 5. Use the function to find conversion paths between expressions.

This could be interesting and offers a more perscriptive way to work with this., but would require a lot of work to make useful.

# Step 1: Define conversion functions
def convert_int_to_float(x: int) -> float:
    return float(x)

def convert_float_to_str(x: float) -> str:
    return str(x)

# Step 2: Create a dictionary of conversion functions
conversion_dict = {
    (int, float): convert_int_to_float,
    (float, str): convert_float_to_str,
}

# Step 3: Implement a unification function
def unify_types(type1, type2):
    if type1 == type2:
        return type1

    if (type1, type2) in conversion_dict:
        return type2

    if (type2, type1) in conversion_dict:
        return type1

    return None

# Step 4: Implement a function to find conversion paths
def find_conversion_path(expr1, expr2):
    type1 = type(expr1)
    type2 = type(expr2)

    common_type = unify_types(type1, type2)
    print(common_type)

    if common_type is None:
        return None

    path = []

    if type1 != common_type:
        path.append(conversion_dict[(type1, common_type)])

    if type2 != common_type:
        path.append(conversion_dict[(common_type, type2)])

    return path

# Step 5: Use the function to find conversion paths between expressions
expr1 = 1
expr2 = 2.0
conversion_path = find_conversion_path(expr1, expr2)

<class 'float'>

test_eq(conversion_path[0], convert_int_to_float)

So, lots of work for kind of a simple thing. TBD if it’s work revisiting in the future.

Exploring class hierarchy

1. Define a function to find the least common ancestor (LCA) of two types in the class hierarchy.
2. Implement a function to find a conversion path between two expressions by finding their LCA and using the LCA to define a conversion function.

I don’t think 2 is generally possible.

# Step 1: Define a function to find the least common ancestor of two types
def least_common_ancestor(type1, type2):
    type1_superclasses = inspect.getmro(type1)
    type2_superclasses = inspect.getmro(type2)
    print(type1_superclasses)
    print(type2_superclasses)

    if type1 in type2_superclasses:
        return type1
    if type2 in type1_superclasses:
        return type2

    for superclass1 in type1_superclasses:
        if superclass1 in type2_superclasses:
            return superclass1

    return None

# Step 2: Implement a function to find a conversion path between two expressions
def find_conversion_path(expr1, expr2):
    type1 = type(expr1)
    type2 = type(expr2)

    common_ancestor = least_common_ancestor(type1, type2)

    if common_ancestor is None:
        # No common ancestor found in the class hierarchy
        return None
    
    def conversion_function(x):
        return common_ancestor(x)

    return conversion_function

# example heirarchy - D is a subclass of C, which is a subclass of A
class A: pass
class B(A): pass
class C(A): pass
class D(C): pass

expr1 = B()
expr2 = D()

conversion_function = find_conversion_path(expr1, expr2)

(<class '__main__.B'>, <class '__main__.A'>, <class 'object'>)
(<class '__main__.D'>, <class '__main__.C'>, <class '__main__.A'>, <class 'object'>)

least_common_ancestor(B, D)

(<class '__main__.B'>, <class '__main__.A'>, <class 'object'>)
(<class '__main__.D'>, <class '__main__.C'>, <class '__main__.A'>, <class 'object'>)

__main__.A

test_fail(lambda: conversion_function(expr1))

The above function does not run.

I don’t know if this is generally possible, but the least common ancestor approach is promising. There may be some element of hardcoded vs least common ancestor that would be useful here.