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

support partial application of Kinds #1409

Open
scolsen opened this issue Apr 4, 2022 · 0 comments
Open

support partial application of Kinds #1409

scolsen opened this issue Apr 4, 2022 · 0 comments

Comments

@scolsen
Copy link
Contributor

scolsen commented Apr 4, 2022

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant