Carp icon indicating copy to clipboard operation
Carp copied to clipboard

support partial application of Kinds

Open scolsen opened this issue 3 years ago • 0 comments

Right now, kind resolution is exact; that is, given a context that expects a function f: x -> f x, one cannot pass the partially concrete type: g: x -> R x String where R is a type of higher kind than f x.

This makes it so that some interface resolutions that work in a language like Haskell, don't yet work in Carp. For example (pure here is defined the same as it is in Haskell):

(assert-equal test
  &(the (Result Int String) (Result.Success 0)))
  &(pure 0)

results in the error

I can’t find any implementation for the interface `pure` of type (Fn [Int] (r132 Int)) at line 43, column 32 in '/Users/scottolsen/dev/typeclass/test/instances/result.carp'.

None of the possibilities have the correct signature:
    Result.Applicative.Success.pure : (Fn [a] (Result a b))
    Result.Applicative.Error.pure : (Fn [a] (Result b a)) at /Users/scottolsen/dev/carpclone/core/Test.carp:179:7.

Traceback:
  (defn main [] (let [test (ref (Test.State.init 0 0))] (do (s...) at dummy-file:0:0.
(eval (cons-last (cons-last (cons-last (cons-last (cons-last...) at /Users/scottolsen/dev/carpclone/core/Test.carp:178:3.
(deftest test (assert-equal test (ref (the (Result Int Int) ...) at /Users/scottolsen/dev/typeclass/test/instances/result.carp:20:1.

Given a definition like Fn [a] (R a b) we should assume that b is concrete since it does not appear in the head of the function. That would make this case inferable.

That is, the kind of (R a b) in Fn [a] (R a b) should be unary * -> * and not binary * -> * -> * since b must be inferred outside of the function context and must be assumed to be resolved to some concrete type using other information.

scolsen avatar Apr 04 '22 19:04 scolsen