-
Notifications
You must be signed in to change notification settings - Fork 20
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Subsume type signatures with expression types
- Loading branch information
Oskar Wickström
committed
Jan 24, 2016
1 parent
93a563a
commit 5e8188e
Showing
9 changed files
with
306 additions
and
84 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,63 @@ | ||
| {-# LANGUAGE FlexibleInstances #-} | ||
| {-# LANGUAGE GeneralizedNewtypeDeriving #-} | ||
| {-# LANGUAGE TypeSynonymInstances #-} | ||
| module Oden.Infer.Substitution where | ||
|
|
||
| import Oden.Type.Polymorphic | ||
| import Oden.Core as Core | ||
|
|
||
| import qualified Data.Set as Set | ||
| import qualified Data.Map as Map | ||
|
|
||
| newtype Subst = Subst (Map.Map TVar Type) | ||
| deriving (Eq, Ord, Show, Monoid) | ||
|
|
||
| -- | The empty substitution | ||
| emptySubst :: Subst | ||
| emptySubst = mempty | ||
|
|
||
| -- | Compose substitutions | ||
| compose :: Subst -> Subst -> Subst | ||
| (Subst s1) `compose` (Subst s2) = Subst $ Map.map (apply (Subst s1)) s2 `Map.union` s1 | ||
|
|
||
| class FTV a => Substitutable a where | ||
| apply :: Subst -> a -> a | ||
|
|
||
| instance Substitutable Type where | ||
| apply _ TAny = TAny | ||
| apply _ (TCon a) = TCon a | ||
| apply (Subst s) t@(TVar a) = Map.findWithDefault t a s | ||
| apply s (TNoArgFn t) = TNoArgFn (apply s t) | ||
| apply s (t1 `TFn` t2) = apply s t1 `TFn` apply s t2 | ||
| apply s (TUncurriedFn as r) = TUncurriedFn (map (apply s) as) (apply s r) | ||
| apply s (TVariadicFn as v r) = TVariadicFn (map (apply s) as) (apply s v) (apply s r) | ||
| apply s (TSlice t) = TSlice (apply s t) | ||
|
|
||
|
|
||
| instance Substitutable Scheme where | ||
| apply (Subst s) (Forall as t) = Forall as $ apply s' t | ||
| where s' = Subst $ foldr Map.delete s as | ||
|
|
||
| instance FTV Core.CanonicalExpr where | ||
| ftv (sc, expr) = ftv sc `Set.union` ftv expr | ||
|
|
||
| instance Substitutable Core.CanonicalExpr where | ||
| apply s (sc, expr) = (apply s sc, apply s expr) | ||
|
|
||
| instance FTV (Core.Expr Type) where | ||
| ftv = ftv . Core.typeOf | ||
|
|
||
| instance Substitutable (Core.Expr Type) where | ||
| apply s (Core.Symbol x t) = Core.Symbol x (apply s t) | ||
| apply s (Core.Application f p t) = Core.Application (apply s f) (apply s p) (apply s t) | ||
| apply s (Core.NoArgApplication f t) = Core.NoArgApplication (apply s f) (apply s t) | ||
| apply s (Core.UncurriedFnApplication f p t) = Core.UncurriedFnApplication (apply s f) (apply s p) (apply s t) | ||
| apply s (Core.Fn x b t) = Core.Fn x (apply s b) (apply s t) | ||
| apply s (Core.NoArgFn b t) = Core.NoArgFn (apply s b) (apply s t) | ||
| apply s (Core.Let x e b t) = Core.Let x (apply s e) (apply s b) (apply s t) | ||
| apply s (Core.Literal l t) = Core.Literal l (apply s t) | ||
| apply s (Core.If c tb fb t) = Core.If (apply s c) (apply s tb) (apply s fb) (apply s t) | ||
| apply s (Core.Slice es t) = Core.Slice (apply s es) (apply s t) | ||
|
|
||
| instance Substitutable a => Substitutable [a] where | ||
| apply = map . apply |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,69 @@ | ||
| module Oden.Infer.Subsumption ( | ||
| Subsuming, | ||
| SubsumptionError(..), | ||
| subsume, | ||
| subsumeTypeSignature | ||
| ) where | ||
|
|
||
| import Oden.Type.Polymorphic | ||
| import Oden.Core as Core | ||
| import Oden.Infer.Substitution | ||
|
|
||
| import qualified Data.Map as Map | ||
|
|
||
| data SubsumptionError = SubsumptionError Type Type | ||
| deriving (Show, Eq) | ||
|
|
||
| class Subsuming s where | ||
| subsume :: s -> s -> Either SubsumptionError s | ||
|
|
||
| subsumeTypeSignature :: Scheme -> Core.Expr Type -> Either SubsumptionError Core.CanonicalExpr | ||
| subsumeTypeSignature s@(Forall _ st) expr = do | ||
| subst <- getSubst st (Core.typeOf expr) | ||
| return (s, apply subst expr) | ||
| where | ||
| getSubst :: Type -> Type -> Either SubsumptionError Subst | ||
| getSubst t (TVar tv) = return (Subst (Map.singleton tv t)) | ||
| getSubst (TFn a1 r1) (TFn a2 r2) = do | ||
| a <- getSubst a1 a2 | ||
| r <- getSubst r1 r2 | ||
| return (a `compose` r) | ||
| getSubst (TNoArgFn r1) (TNoArgFn r2) = getSubst r1 r2 | ||
| getSubst (TUncurriedFn a1 r1) (TUncurriedFn a2 r2) = do | ||
| as <- mapM (uncurry getSubst) ((r1, r2) : zip a1 a2) | ||
| return (foldl compose emptySubst as) | ||
| getSubst (TVariadicFn a1 v1 r1) (TVariadicFn a2 v2 r2) = do | ||
| as <- mapM (uncurry getSubst) ((r1, r2) : (v1, v2) : zip a1 a2) | ||
| return (foldl compose emptySubst as) | ||
| getSubst TAny _ = return emptySubst | ||
| getSubst t1 t2 | ||
| | t1 == t2 = return emptySubst | ||
| | otherwise = Left (SubsumptionError t1 t2) | ||
|
|
||
| instance Subsuming Type where | ||
| TAny `subsume` TAny = Right TAny | ||
| t `subsume` TAny = Left (SubsumptionError t TAny) | ||
| TAny `subsume` _ = Right TAny | ||
| t1@(TNoArgFn at1) `subsume` (TNoArgFn at2) = do | ||
| _ <- at1 `subsume` at2 | ||
| return t1 | ||
| t1@(TFn at1 rt1) `subsume` (TFn at2 rt2) = do | ||
| _ <- at1 `subsume` at2 | ||
| _ <- rt1 `subsume` rt2 | ||
| return t1 | ||
| t1@(TUncurriedFn ats1 rt1) `subsume` (TUncurriedFn ats2 rt2) = do | ||
| mapM_ (uncurry subsume) (zip ats1 ats2) | ||
| _ <- rt1 `subsume` rt2 | ||
| return t1 | ||
| t1@(TVariadicFn ats1 vt1 rt1) `subsume` (TVariadicFn ats2 vt2 rt2) = do | ||
| mapM_ (uncurry subsume) (zip ats1 ats2) | ||
| _ <- vt1 `subsume` vt2 | ||
| _ <- rt1 `subsume` rt2 | ||
| return t1 | ||
| t1@(TSlice st1) `subsume` (TSlice st2) = do | ||
| _ <- st1 `subsume` st2 | ||
| return t1 | ||
| t1 `subsume` t2 | ||
| | t1 == t2 = Right t1 | ||
| | otherwise = Left (SubsumptionError t1 t2) | ||
|
|
Oops, something went wrong.