summaryrefslogtreecommitdiff
path: root/lambda-calcul/haskell/src/Minilang/Lambda
diff options
context:
space:
mode:
Diffstat (limited to 'lambda-calcul/haskell/src/Minilang/Lambda')
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs4
-rw-r--r--lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs11
2 files changed, 13 insertions, 2 deletions
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
index 2e1814e..ab590c6 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Infer.hs
@@ -14,6 +14,7 @@ import GHC.Generics (Generic)
import qualified Minilang.Lambda.Eval as Eval
import Minilang.Lambda.Unify (Type (..), UnifyError, apply, unify)
import Prelude hiding (lookup)
+import qualified Minilang.Lambda.Unify as Unify
data ATerm ann
= Var Text ann
@@ -25,6 +26,9 @@ data TypeError
= UnifyError UnifyError
deriving (Show, Eq)
+render :: TypeError -> Text
+render (UnifyError ue) = Unify.render ue
+
fromTerm :: Eval.Term -> ATerm ()
fromTerm (Eval.Var x) = Var x ()
fromTerm (Eval.Lam x body) = Lam x (fromTerm body) ()
diff --git a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
index f3fff04..96e9990 100644
--- a/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
+++ b/lambda-calcul/haskell/src/Minilang/Lambda/Unify.hs
@@ -46,10 +46,17 @@ apply subs t =
foldr (\(x, s) -> subst s x) t subs
data UnifyError
- = MismatchHead Text Text [Type] [Type]
- | Circularity Identifier Type
+ = Circularity Identifier Type
deriving (Show, Eq)
+render :: UnifyError -> Text
+render (Circularity x t) =
+ "Cannot unify type variable "
+ <> x
+ <> " with type "
+ <> pretty t
+ <> " due to circularity: The variable already occurs in the type."
+
unifyOne :: Type -> Type -> Either UnifyError Substitution
unifyOne (TyVar x) (TyVar y) = if x == y then Right [] else Right [(x, TyVar y)]
unifyOne (f :-> g) (f' :-> g') =