search

lexi-lambda / hackett

WIP implementation of a Haskell-like Lisp in Racket
https://lexi-lambda.github.io/hackett/
ISC License
1.17k stars 50 forks source link

Functor Instance Misbehaving #64

Closed howell closed 6 years ago

howell commented 6 years ago

I've stared really hard at these few lines and can't think of any explanation for why the instance doesn't typecheck while tl-map does:

(data (TwoLists A)
      (TwoLists (List A) (List A)))

(defn tl-map : (∀ [A B] {{A -> B} -> (TwoLists A) -> (TwoLists B)})
  [[f (TwoLists l1 l2)]
   (TwoLists (map f l1) (map f l2))])

(instance (∀ [A] (Functor (TwoLists A)))
  [map tl-map])

typechecker: type mismatch
  between: (TwoLists A22)
      and: TwoLists in: tl-map
lexi-lambda commented 6 years ago

Hackett is a higher-kinded language, but it doesn’t currently have a kindchecker. In that sense, Hackett is statically typed but dynamically kinded. Your program has a kind error, namely that Functor expects a type of kind * -> * (or Type -> Type if you prefer), but (TwoLists A) has kind *.

The proper error here is a kind error, but because Hackett doesn’t know about kinds, you get an error when the typechecker attempts to unify (TwoLists A22) with TwoLists. This is itself ill-kinded, given that those two types have different kinds, which is a good clue that the issue is related to kindedness without the presence of better error reporting.

lexi-lambda commented 6 years ago

After I wrote that comment, I realized I didn’t actually mention the solution. In case it wasn’t clear, I think your program will typecheck if you change (instance (forall [A] (Functor (TwoLists A))) ....) to (instance (Functor TwoLists) ....) (though I have not actually tested it).

howell commented 6 years ago

Ah yeah of course. Thanks for pointing that out!