checkpoint

parser.pl

@@ -52,14 +52,25 @@ build_ast([id(match), Expr, ClausesSExpr], match(Expr, Clauses)) :-
 build_ast([id(tuple) | Elements], tuple(Elements)) :- !.
 build_ast([id(list) | Elements], list_val(Elements)) :- !.
 
-% Function application (must be last among id-starting rules for simple names)
+% Function application (id as functor)
-build_ast([id(FunctorName) | Args], Application) :-
+build_ast([id(FunctorName) | Args], apply(id(FunctorName), Args)) :-
-    atom(FunctorName), % Ensure FunctorName is an atom, not a complex term
+    atom(FunctorName), % Ensure FunctorName is an atom
-    Application =.. [FunctorName | Args], !.
+    !.
 
 % Higher-order function application: ((lambda (x) x) 10) or (VarHoldingLambda 10)
 % Head of ItemsList is a complex AST (e.g., lambda(...), id(Var))
-build_ast([FunctorSExpr | Args], apply(FunctorSExpr, Args)) :- Args \= [], !. % Ensure there are arguments
+% This rule now also handles ((lambda () body)) correctly as Args can be [].
+build_ast([FunctorSExpr | Args], apply(FunctorSExpr, Args)) :-
+    % FunctorSExpr is not an id, or the previous rule for id functor would have caught it.
+    % Or, FunctorSExpr is an id, but it's the *only* thing in the list, e.g. (my_var) -> id(my_var) not apply(id(my_var),[])
+    % The s_expression(id(Atom)) rule handles single identifiers like (my_var) -> id(my_var).
+    % So, if we are here with [id(X)], it means it's (X) which should be id(X).
+    % This rule is for (F Args...) where F is complex, or (F) where F is complex.
+    % If Items is [SomeComplexAST], it should become apply(SomeComplexAST, []) if it's meant to be a call.
+    % Or generic_list([SomeComplexAST]) if it's just a list with one complex item.
+    % The current s_expression_items structure means Args will be a list.
+    % If (F) is parsed, Items = [FunctorSExpr], so Args = [].
+    !.
 
 % Generic list structure if not a keyword or application, e.g. for parameters or clause pairs
 % Also handles (X) where X is a complex term, parsing to generic_list([X])
@@ -69,12 +80,25 @@ build_ast([], list_nil) :- !. % Should have been caught by s_expression(list_nil
 % --- Helpers for AST construction ---
 
 % extract_lambda_params(SExpr_representing_param_list, PrologListOfParamNames)
-% SExpr for (p1 p2 ...): generic_list([id(p1), id(p2), ...])
+extract_lambda_params(list_nil, []) :- !. % Case: (lambda () body) -> ParamsSExpr = list_nil
+
+extract_lambda_params(id(AtomParam), [AtomParam]) :- % Case: (lambda x body) -> ParamsSExpr = id(x)
+    atom(AtomParam),
+    get_id_name_from_ast(id(AtomParam), AtomParam), !. % Ensures AtomParam is indeed the name.
+
+% Case: (lambda (p1 p2 ...) body)
+% ParamsSExpr will be apply(id(p1), [id(p2), ...]) due to updated build_ast rules.
+extract_lambda_params(apply(id(PHead), PArgASTs), [PHead | PArgNames]) :-
+    atom(PHead),
+    is_list(PArgASTs),
+    maplist(get_id_name_from_ast, PArgASTs, PArgNames), !.
+
+% Fallback for safety, or if (lambda (generic_list_form_params) body) is ever valid.
+% This clause might be dead code for typical lambda parameter lists now.
 extract_lambda_params(generic_list(IdASTs), ParamNames) :-
+    log(parser_warning, 'Lambda parameters parsed as generic_list, check usage: ~w', [generic_list(IdASTs)]),
     maplist(get_id_name_from_ast, IdASTs, ParamNames), !.
-extract_lambda_params(list_nil, []) :- !. % (lambda () body)
+
-extract_lambda_params(id(ParamAST_single_param), [ParamName]) :- % (lambda x body)
-    get_id_name_from_ast(id(ParamAST_single_param), ParamName), !.
 
 get_id_name_from_ast(id(Name), Name).
 
@@ -86,9 +110,14 @@ extract_match_clauses(generic_list(ClauseSExprs), ClauseASTs) :-
 extract_match_clauses(list_nil, []) :- !. % (match expr ()) - no clauses
 
 % parse_one_match_clause(SExpr_for_one_clause, clause(PatternAST, true, BodyAST))
-% SExpr for (pat body): generic_list([RawPatternAST, BodyAST])
+% SExpr for (pat body) will be parsed as apply(RawPatternAST, [BodyAST])
-parse_one_match_clause(generic_list([RawPatternAST, BodyAST]), clause(Pattern, true, BodyAST)) :-
+parse_one_match_clause(apply(RawPatternAST, [BodyAST]), clause(Pattern, true, BodyAST)) :-
-    ast_to_pattern(RawPatternAST, Pattern).
+    ast_to_pattern(RawPatternAST, Pattern), !.
+% Handle case where a clause might be a single item, e.g. (match x (DefaultCaseBody)) - not standard LISP match
+parse_one_match_clause(BodyAST, clause(pwild, true, BodyAST)) :-
+    log(parser_warning, 'Match clause parsed as single body term, assuming wildcard pattern: ~w', [BodyAST]).
+    % This assumes that if a clause is not apply(Pat, [Body]), it's just a Body for a wildcard.
+    % This might need refinement based on desired match syntax for single-element clauses.
 
 ast_to_pattern(id(Name), pvar(Name)) :- Name \= '_', !.
 ast_to_pattern(id('_'), pwild) :- !.

run_tests.pl

@@ -0,0 +1,20 @@
+#!/usr/bin/env swipl
+
+:- initialization(main, main).
+
+:- consult(log).
+:- consult(parser).
+:- consult(types).
+:- consult(tests).
+
+main(_Argv) :-
+    log:set_verbosity(1), % Default verbosity for tests, can be overridden
+    ( current_prolog_flag(argv, [VerbosityArg | _Tail]), atom_string(VerbosityAtom, VerbosityArg), atom_number(VerbosityAtom, VerbosityLevel) ->
+        log:set_verbosity(VerbosityLevel),
+        format(user_error, 'Verbosity set to ~w from command line.~n', [VerbosityLevel])
+    ; format(user_error, 'Using default verbosity 1. Provide a number (0-2) as arg to change.~n', [])
+    ),
+    tests:run_tests,
+    halt.
+main(_) :- % Fallback if run_tests fails or no args
+    halt(1).

tests.pl

@@ -129,6 +129,95 @@ run_tests :-
             boolean
             ),
 
+    % --- Function Type Tests ---
+    run_test('Lambda returning number',
+             EmptyEnv,
+             "(lambda (x) 10)", % x is any, body is 10 (number)
+             fun_type([any], number)
+            ),
+
+    run_test('Lambda identity function',
+             EmptyEnv,
+             "(lambda (x) x)",   % x is any, body is x (any)
+             fun_type([any], any)
+            ),
+
+    run_test('Lambda with two params, returning one',
+             EmptyEnv,
+             "(lambda (x y) y)", % x,y are any, body is y (any)
+             fun_type([any, any], any)
+            ),
+            
+    run_test('Lambda with no params, returning string',
+             EmptyEnv,
+             "(lambda () \"hello\")",
+             fun_type([], string)
+            ),
+
+    run_test('Apply identity lambda to number',
+             EmptyEnv,
+             "((lambda (x) x) 10)", % (lambda (x) x) -> fun_type([any],any). Applied to 10 (number). Result: any.
+             any
+            ),
+
+    run_test('Apply lambda returning number',
+             EmptyEnv,
+             "((lambda (x) 10) \"text\")", % (lambda (x) 10) -> fun_type([any],number). Applied to "text" (string). Result: number.
+             number
+            ),
+
+    run_test('Apply lambda with no params',
+             EmptyEnv,
+             "((lambda () \"world\"))", % fun_type([], string) applied to (). Result: string.
+             string
+            ),
+
+    run_test('Apply lambda with arity mismatch (too few args)',
+             EmptyEnv,
+             "((lambda (x y) x) 10)", % fun_type([any,any],any) applied to (10). Arity mismatch.
+             never % Or error specific representation
+            ),
+
+    run_test('Apply lambda with arity mismatch (too many args)',
+             EmptyEnv,
+             "((lambda (x) x) 10 20)", % fun_type([any],any) applied to (10, 20). Arity mismatch.
+             never % Or error specific representation
+            ),
+
+    run_test('Apply non-function (number)',
+             EmptyEnv,
+             "(10 20)", % AST: apply(int(10), [int(20)])
+             never % Or error specific representation
+            ),
+
+    run_test('Apply variable holding a function',
+             [f:fun_type([number], string)],
+             "(f 123)", % f is fun_type([number],string). Applied to 123 (number). Result: string.
+             string % This test will require unification of number with number for param.
+            ),
+
+    run_test('Apply variable holding a function - arg type mismatch (placeholder)',
+             [id_fun:fun_type([number], number)], % Expects number
+             "(id_fun \"text\")", % Called with string. Current 'any' in lambda def won't catch this.
+                                  % If id_fun was defined as (lambda (x::number) x), this would be 'never'.
+                                  % For now, if ExpectedParamType is 'number' and Actual is 'string',
+                                  % compatible_arg_types should fail if unify_types(number, string, union(...))
+                                  % and we check UnifiedType \= never.
+                                  % Let's assume unify_types(number, string, union(number,string))
+                                  % union(number,string) \= never, so this would pass if we don't check for subtype.
+                                  % Let's refine compatible_arg_types to be stricter or unify_types to return never for incompatible base types.
+                                  % For now, let's assume the current unify_types(T1,T2,union(T1,T2)) for disparate types.
+                                  % And compatible_arg_types checks `UnifiedType \= never`.
+                                  % This test will pass with `number` if `id_fun` is `fun_type([any],number)`.
+                                  % If `id_fun` is `fun_type([number],number)`, then `unify_types(number, string, union(number,string))`
+                                  % `union(number,string) \= never` is true.
+                                  % The rule `unify_types(T1, T2, union(T1, T2))` needs to be before any catch-all.
+                                  % The `compatible_arg_types` should ideally be `unify_types(Expected, Actual, Expected)`
+                                  % or `unify_types(Expected, Actual, Unified)` and `is_subtype(Unified, Expected)`.
+                                  % Let's adjust `compatible_arg_types` for stricter checking.
+             never % Expecting failure due to type mismatch.
+            ),
+
     log(tests, 'Test suite finished.').
 
 % To run:

todo.md

@@ -0,0 +1,121 @@
+# Todo: Enhancing the Language for Type-Checking and Elixir Transpilation
+
+This document outlines the features and improvements required to enable robust type-checking for our language and to facilitate its transpilation into readable Elixir code.
+
+## I. Type System Enhancements (Likely impacts `types.pl`, `parser.pl`)
+
+- [ ] **Define Core Types:**
+    - [ ] Formalize basic types: Integer, Float, String, Boolean.
+    - [ ] Add support for Elixir-idiomatic types: Atoms/Symbols.
+    - [ ] Define collection types: Lists, Maps (Hash-like structures).
+    - [ ] Add support for Tuples.
+- [ ] **Advanced Type Features:**
+    - [ ] Implement Algebraic Data Types (ADTs) / Tagged Unions (e.g., `{:ok, value} | {:error, reason}`).
+    - [ ] Introduce Structs/Records with named, typed fields.
+    - [ ] Define Function Types (signatures for first-class functions).
+    - [ ] Explore Generics/Parametric Polymorphism.
+- [ ] **Type Annotations:**
+    - [ ] Design syntax for type annotations for variables.
+    - [ ] Design syntax for type annotations for function parameters.
+    - [ ] Design syntax for type annotations for function return types.
+    - [ ] Update `parser.pl` to parse these new syntax elements.
+- [ ] **Type System Semantics:**
+    - [ ] Define subtyping rules (if applicable).
+    - [ ] Define type compatibility and coercion rules.
+
+## II. Type Checker Implementation (Likely new modules, parts in `types.pl`)
+
+- [ ] **AST (Abstract Syntax Tree) Enhancements:**
+    - [ ] Ensure AST nodes (from `parser.pl`) can carry or be decorated with type information.
+- [ ] **Type Inference:**
+    - [ ] Implement a type inference algorithm (e.g., Hindley-Milner subset or simpler local inference).
+- [ ] **Type Checking Algorithm:**
+    - [ ] Develop a traversal algorithm for the AST to verify type correctness.
+    - [ ] Create a type environment to store and look up type information for symbols (variables, functions).
+- [ ] **Error Reporting:**
+    - [ ] Implement clear and informative type error messages, including source locations.
+- [ ] **Module System Integration:**
+    - [ ] Ensure the type checker correctly handles types across modules/namespaces if the language supports them.
+
+## III. Elixir Transpiler Development (Likely new modules/scripts, e.g., `transpiler.pl`)
+
+- [ ] **AST to Elixir AST Mapping:**
+    - [ ] Define a clear mapping from the source language AST nodes to Elixir AST constructs.
+    - [ ] Handle lexical scoping and variable declarations, considering Elixir's scoping rules.
+- [ ] **Code Generation:**
+    - [ ] Implement a code generator that produces readable Elixir source code from the target Elixir AST.
+    - [ ] Focus on generating idiomatic Elixir code.
+- [ ] **Mapping Language Constructs:**
+    - [ ] **Functions:**
+        - [ ] Map function definitions to Elixir `def`/`defp`.
+        - [ ] Handle function calls, arity, and default arguments.
+        - [ ] Map anonymous functions/lambdas.
+    - [ ] **Control Flow:**
+        - [ ] Map conditional statements (if/else) to Elixir `if/else`, `cond`, or `case`.
+        - [ ] Map loops (e.g., `for`, `while` in Perl) to Elixir's recursion, comprehensions, or `Enum` module functions.
+    - [ ] **Data Structures:**
+        - [ ] Map source language lists/arrays to Elixir lists.
+        - [ ] Map source language hashes/maps to Elixir maps.
+        - [ ] Map structs/records (if added) to Elixir structs or maps.
+        - [ ] Map tuples (if added) to Elixir tuples.
+    - [ ] **Operators:**
+        - [ ] Map arithmetic, logical, and comparison operators, noting any semantic differences.
+    - [ ] **Modules/Namespaces:**
+        - [ ] Map source language modules/namespaces to Elixir `defmodule`.
+        - [ ] Handle imports/exports (`require`, `import`, `alias` in Elixir).
+- [ ] **Standard Library Mapping:**
+    - [ ] Identify core functions in the source language's standard library.
+    - [ ] Provide Elixir equivalents or implement shims/wrappers in Elixir.
+- [ ] **Error Handling:**
+    - [ ] Map error handling mechanisms (e.g., `die`/`warn`, exceptions in Perl) to Elixir's `try/rescue/catch` or idiomatic error tuples (`{:ok, ...}` / `{:error, ...}`).
+- [ ] **Comments and Formatting:**
+    - [ ] Investigate preserving comments from source to target Elixir code.
+    - [ ] Implement basic code formatting for generated Elixir, or leverage Elixir's own formatter.
+
+## IV. Language Features for Elixir Compatibility (Impacts `parser.pl`, `types.pl`)
+
+- [ ] **Immutability:**
+    - [ ] Analyze current mutability semantics. Perl is highly mutable.
+    - [ ] Encourage or enforce immutability for data structures where possible to align with Elixir.
+    - [ ] Provide clear strategies for handling state if mutable constructs are kept or how they map to Elixir's process state or other patterns.
+- [ ] **Pattern Matching:**
+    - [ ] Consider adding or enhancing pattern matching capabilities in the source language, as it's central to Elixir.
+    - [ ] Update `parser.pl` and type checker for any new pattern matching syntax.
+- [ ] **Concurrency:**
+    - [ ] If the source language has concurrency features, plan how to map them to Elixir's actor model (Processes, GenServers, Tasks).
+    - [ ] If not, consider if adding high-level concurrency constructs inspired by Elixir is feasible or desirable.
+- [ ] **Truthiness/Falsiness:**
+    - [ ] Define clear mapping for Perl's flexible truthy/falsy values to Elixir's stricter `false` and `nil`.
+
+## V. Specific Perl-to-Elixir Considerations
+
+- [ ] **Perlisms:**
+    - [ ] Identify common Perl idioms and determine how they will be handled (e.g., context sensitivity like scalar/list context, implicit variables like `$_`, ` @_`). This is a major challenge.
+    - [ ] Decide on a strategy for Perl's extensive built-in functions and special variables. Many might not have direct Elixir equivalents.
+- [ ] **Regular Expressions:**
+    - [ ] Map Perl's powerful regex features and syntax to Elixir's `Regex` module.
+- [ ] **References:**
+    - [ ] Determine how Perl references (to scalars, arrays, hashes, etc.) will be handled. Elixir does not have direct pointer-like references in the same way; this might involve transforming data structures or using process dictionaries/ETS carefully.
+- [ ] **Sigils:**
+    - [ ] Decide how Perl's sigils (`$`, `@`, `%`) will be treated. They might be dropped if type information makes them redundant, or mapped to naming conventions.
+
+## VI. Tooling and Infrastructure
+
+- [ ] **Build Process:**
+    - [ ] Integrate type checking and transpilation into the build/compilation pipeline.
+- [ ] **Testing (Extend `tests.pl` or new test suites):**
+    - [ ] Add tests specifically for the type checker (unit tests for type rules, integration tests).
+    - [ ] Add tests for the transpiler:
+        - [ ] Unit tests for individual construct mappings.
+        - [ ] Property-based tests if applicable.
+        - [ ] End-to-end tests: compile source language code, transpile to Elixir, run the Elixir code, and verify output/behavior.
+- [ ] **Documentation:**
+    - [ ] Document the new type system (supported types, annotation syntax).
+    - [ ] Document how to write code in the source language that transpiles effectively and idiomatically to Elixir.
+    - [ ] Document known limitations or tricky areas of the transpiler.
+- [ ] **Debugging Support (`log.pl`):**
+    - [ ] Enhance `log.pl` or add new logging for debugging the type checker and transpiler.
+    - [ ] Consider source map generation if feasible for debugging transpiled code.
+
+This list is a comprehensive starting point and will likely evolve as development progresses and more is understood about the existing codebase and specific challenges.
+The files `parser.pl` and `types.pl` are expected to see significant changes. New modules for transpilation (e.g., `transpiler.pl` or similar) will need to be created. `tests.pl` will need to be expanded significantly.

type_check_file.pl

@@ -0,0 +1,48 @@
+#!/usr/bin/env swipl
+
+:- initialization(main, main).
+
+:- consult(log).
+:- consult(parser).
+:- consult(types).
+
+main(Args) :-
+    log:set_verbosity(1), % Default verbosity, can be adjusted
+    ( Args = [FilePath | VerbosityArgs] ->
+        ( VerbosityArgs = [VerbosityArg | _], atom_string(VerbosityAtom, VerbosityArg), atom_number(VerbosityAtom, VLevel) ->
+            log:set_verbosity(VLevel),
+            format(user_error, 'Verbosity set to ~w from command line.~n', [VLevel])
+        ; format(user_error, 'Using default verbosity 1. Add a number (0-2) after filepath to change.~n', [])
+        ),
+        type_check_file(FilePath)
+    ; writeln(user_error, 'Usage: type_check_file.pl <filepath> [verbosity_level]'),
+      halt(1)
+    ).
+
+type_check_file(FilePath) :-
+    ( exists_file(FilePath) ->
+        read_file_to_string(FilePath, CodeString, []),
+        format(user_output, "--- Type Checking File: ~w ---~n", [FilePath]),
+        format(user_output, "Code:~n~s~n~n", [CodeString]),
+        ( parser:parse(CodeString, AST) ->
+            format(user_output, "Parsed AST: ~w~n", [AST]),
+            types:initial_env(EmptyEnv),
+            ( catch(types:infer_type(AST, EmptyEnv, InferredType), Error, (
+                log:log(error, caught_error_in_type_check_file(Error)),
+                log:explain_error(Error, Explanation),
+                format(user_output, "Type Inference Error: ~w~n", [Explanation]),
+                InferredType = error(Error) % Represent error
+                )) -> true
+            ; InferredType = 'inference_failed_silently_in_type_check_file'
+            ),
+            format(user_output, "~n--- Inferred Type for the whole expression ---~n~w~n~n", [InferredType]),
+            ( InferredType = error(_) ; InferredType = 'inference_failed_silently_in_type_check_file' ->
+                halt(1)
+            ; halt(0)
+            )
+        ; format(user_error, "Parse FAILED for file: ~w~n", [FilePath]),
+          halt(1)
+        )
+    ; format(user_error, "File not found: ~w~n", [FilePath]),
+      halt(1)
+    ).

types.pl

@@ -6,6 +6,7 @@
       % Type representations (examples)
       type_number/0, type_string/0, type_boolean/0, type_list_nil/0,
       type_list/1, type_tuple/1, type_union/2, type_intersection/2, type_negation/1,
+      type_fun/2, % Added for function types
       type_any/0, type_never/0,
       initial_env/1
     ]).
@@ -24,6 +25,7 @@ type_tuple(Ts) :- _ = tuple(Ts), is_list(Ts). % Ts is used, not singleton
 type_union(T1, T2) :- _ = union(T1, T2). % T1, T2 are used, not singletons
 type_intersection(T1, T2) :- _ = intersection(T1, T2). % T1, T2 are used, not singletons
 type_negation(T) :- _ = negation(T). % T is used, not singleton
+type_fun(PTs, RT) :- _ = fun_type(PTs, RT), is_list(PTs). % PTs, RT are used
 type_any :- _ = any. % Top type
 type_never :- _ = never. % Bottom type, result of failed branches or contradictions
 
@@ -92,25 +94,61 @@ infer_type(is_number(ArgAst), Env, boolean) :-
     log(type_inference, 'Inferring type for is_number/1 call'),
     infer_type(ArgAst, Env, _ArgType). % ArgType can be anything, is_number checks it.
 
-% Lambda expressions (placeholder - full function type inference is complex)
+% Lambda expressions
-infer_type(lambda(_Params, _BodyAst), _Env, any) :- % For (lambda (params...) body)
+infer_type(lambda(Params, BodyAst), EnvIn, fun_type(ParamTypes, ReturnType)) :-
-    % A proper implementation would construct a function type: fun_type(ParamTypes, ReturnType)
+    log(type_inference, 'Inferring type for lambda expression'),
-    % This requires inferring types for params (possibly from annotations) and body.
+    length(Params, Arity),
-    log(type_inference, 'Lambda expression -> any (placeholder)').
+    length(ParamTypes, Arity),
+    maplist(=(any), ParamTypes), % Assume 'any' type for params for now
+    build_env_for_lambda_body(Params, ParamTypes, EnvIn, EnvForBody),
+    log(type_inference, lambda_params_env(Params, ParamTypes, EnvForBody)),
+    infer_type(BodyAst, EnvForBody, ReturnType),
+    log(type_inference, lambda_body_type(ReturnType) -> fun_type(ParamTypes, ReturnType)).
 
-% General function application (placeholder - requires function type for FunctorSExpr)
+build_env_for_lambda_body([], [], Env, Env).
-infer_type(apply(FunctorSExpr, ArgsSExprs), Env, any) :- % For ((lambda ...) arg) or (f arg) where f is complex
+build_env_for_lambda_body([Param|ParamsRest], [ParamType|ParamTypesRest], EnvIn, EnvOut) :-
-    log(type_inference, 'General application (apply/2) -> any (placeholder)'),
+    refine_env(Param, ParamType, EnvIn, EnvMid), % refine_env shadows existing bindings
-    infer_type(FunctorSExpr, Env, FunctorType),
+    build_env_for_lambda_body(ParamsRest, ParamTypesRest, EnvMid, EnvOut).
-    % Infer types of ArgsSExprs
+
-    maplist(infer_type_arg(Env), ArgsSExprs, ArgTypes),
+% General function application
-    log(type_inference, apply_functor_type(FunctorType)),
+infer_type(apply(FunctorAst, ArgsAsts), Env, ResultType) :-
-    log(type_inference, apply_arg_types(ArgTypes)).
+    log(type_inference, 'Inferring type for function application'),
-    % A proper implementation would:
+    infer_type(FunctorAst, Env, FunctorType),
-    % 1. Ensure FunctorType is a function type, e.g., fun_type(ExpectedParamTypes, ReturnType).
+    maplist(infer_type_arg(Env), ArgsAsts, ActualArgTypes),
-    % 2. Check Arity and if ArgTypes are subtypes of ExpectedParamTypes.
+    log(type_inference, apply_functor(FunctorAst) -> FunctorType),
-    % 3. Return ReturnType.
+    log(type_inference, apply_args(ArgsAsts) -> ActualArgTypes),
-    % For now, it's 'any'.
+    determine_apply_result_type(FunctorType, ActualArgTypes, ResultType).
+
+determine_apply_result_type(fun_type(ExpectedParamTypes, ReturnType), ActualArgTypes, ResultType) :-
+    !, % Matched a function type
+    length(ExpectedParamTypes, Arity),
+    length(ActualArgTypes, Arity), % Check arity
+    compatible_arg_types(ExpectedParamTypes, ActualArgTypes), % Check types
+    ResultType = ReturnType,
+    log(type_inference, apply_success(fun_type(ExpectedParamTypes, ReturnType), ActualArgTypes) -> ReturnType).
+determine_apply_result_type(fun_type(ExpectedParamTypes, _ReturnType), ActualArgTypes, never) :-
+    !, % Arity or type mismatch for a known function type
+    ( length(ExpectedParamTypes, ExpArity), length(ActualArgTypes, ActArity), ExpArity \= ActArity ->
+        log(error, type_error(arity_mismatch(ExpArity, ActArity), apply))
+    ; \+ compatible_arg_types(ExpectedParamTypes, ActualArgTypes) -> % Must be type mismatch
+        log(error, type_error(argument_type_mismatch(ExpectedParamTypes, ActualArgTypes), apply))
+    ; log(error, type_error(unknown_apply_error(fun_type(ExpectedParamTypes, _), ActualArgTypes), apply)) % Should not happen
+    ).
+determine_apply_result_type(any, _ActualArgTypes, any) :-
+    !, % Calling something of type 'any'
+    log(type_inference, apply_to_any_type -> any).
+determine_apply_result_type(OtherType, ActualArgTypes, never) :-
+    % Trying to call a non-function type (e.g., number, string)
+    log(error, type_error(cannot_apply_non_function(OtherType, ActualArgTypes), apply)),
+    explain_error(type_error(cannot_apply_non_function(OtherType), apply), _Msg).
+
+compatible_arg_types([], []).
+compatible_arg_types([ExpectedType|ETs], [ActualType|ATs]) :-
+    unify_types(ExpectedType, ActualType, UnifiedType), % Check if actual can be used where expected is required
+    UnifiedType \= never, % Or more strictly: unify_types(ExpectedType, ActualType, ExpectedType)
+    % unify_types(ExpectedType, ActualType, UnifiedType), UnifiedType \= never, % Original less strict check
+    unify_types(ExpectedType, ActualType, ExpectedType), % Stricter: ActualType must be unifiable to ExpectedType (i.e. subtype or equal)
+    compatible_arg_types(ETs, ATs).
 
 infer_type_arg(Env, ArgSExpr, ArgType) :- infer_type(ArgSExpr, Env, ArgType).