Skip to content

Instantly share code, notes, and snippets.

@lambdageek
Created November 15, 2014 16:47
Show Gist options
  • Save lambdageek/56f7d7846f6505a24bae to your computer and use it in GitHub Desktop.
Save lambdageek/56f7d7846f6505a24bae to your computer and use it in GitHub Desktop.
The gist of ML modules
name: gist-ml
version: 0.1.0.0
synopsis: The gist of ML modules
-- description:
license: BSD3
author: Aleksey Kliger
maintainer: aleksey at lambdageek dot org
-- copyright:
-- category:
build-type: Simple
-- extra-source-files:
cabal-version: >=1.10
library
exposed-modules:
GistML
-- other-modules:
-- other-extensions:
build-depends: base >=4.6 && <4.7,
mtl >= 2.2,
unbound-generics
-- hs-source-dirs:
default-language: Haskell2010
{-#
LANGUAGE
DeriveGeneric, DeriveDataTypeable,
MultiParamTypeClasses,
ViewPatterns
#-}
-- A short example of an ML-style module system atop a core lambda calculus.
--
-- The core expression language has variables, applications and
-- lambdas and constants. The type language has variables (of the single kind *)
-- and function types and some base types.
--
-- To this we add syntax for modules and signatures and expression and type level operations to
-- refer to projected fields of previously defined modules.
--
-- The signatures specify a series of specs. Each spec may be: an abstract type declaration,
-- a manifest type alias, a value declared with its type, or a nested submodule declared with a
-- signature expression. signature expressions are either literal signatures or the identifiers of
-- previously defined signaturs.
--
-- A model is a series of definitions. Each definition may be: a manifest type alias,
-- a value defined to be equal to some expression, or a submodule defined by a module expression.
-- A module expression is either the path into a previously defined model, a literal module definition,
-- or a module expression sealed with a signature expression in order to hide some fields or to hide
-- the definitions of some types.
--
-- A toplevel program consists of a sequence of signature and module definitions.
--
-- Example:
-- signature S1 = { type t : * ; type s = t -> t ; val x : s}
-- signature S2 = { type t : * }
-- module M1 = { type t = Int ; type s = Int -> t}
-- module M2 = (M1 : S2)
module GistML where
import GHC.Generics (Generic)
import Data.Typeable (Typeable)
import Control.Applicative
import Control.Monad.Reader
import Control.Monad.Except
import qualified Data.List
import Unbound.Generics.LocallyNameless
-- ================================================================================
-- Part I: Syntax
-- Section 1 : Fields, Identifiers and Paths
-- A field is the "external" name for a component of a module. It's
-- how other modules talk about each other's visible components.
type Field = String
-- An identifier is associated with a module, but
-- it substituted by paths.
type Ident = Name Path
-- A path picks out a submodule from the module associated with its
-- root ident.
data Path = Id Ident
| Project Path Field
deriving (Show, Generic, Typeable)
-- Signature identifiers are associated with signatures. They're not
-- particularly interesting because they just form a flat namespace at the toplevel.
type SigIdent = Name SigPath
data SigPath = SigIdent SigIdent
deriving (Show, Generic, Typeable)
-- Section 2 : Core language.
-- Variables stand for expressions.
type Var = Name Expr
-- A ValuePath is a Path (which picks out a module) together with a
-- Field that picks out a value component of that module.
data ValuePath = ValuePath Path Field
deriving (Show, Generic, Typeable)
data Expr =
-- core language stuff
V Var
| I Integer
| App Expr Expr
| Lam (Bind (Var, Embed Type) Expr)
-- reference to another module's values.
| P ValuePath
deriving (Show, Generic, Typeable)
-- Type variables stand for types.
type TyVar = Name Type
-- Pick out a type component of a module path.
data TypePath = TypePath Path Field
deriving (Show, Generic, Typeable)
data Type =
-- core language types
TV TyVar
| TInt
| Arr Type Type
-- refernce to another module's types
| TP TypePath
deriving (Show, Generic, Typeable)
-- Could have more kinds, but this simple example just has *
data Kind = KType
deriving (Show, Generic, Typeable)
-- Section 3 : Signatures
-- A signature is like the type of a module.
-- One of the insights of the ML module system is that a signature is
-- like a record type {field1: ty1, ... fieldN: tyN} except that later
-- some of the fields may in fact be either abstract or manifest type
-- declarations, and later fields may depend on previous type fields.
-- To deal with this, each (type) field in a signature has both an extranal field name,
-- and an internal type variable that is bound in the rest of the signature.
-- There can also be nested submodules, in which case the external name is a field name,
-- and the internal
data Sig
=
-- trivial empty signature
NilSig
-- { val f : T, sig }
| ValSig Field Type Sig
-- { type f : TypeSpec, a. Sig } where Sig may use "a" to refer to TypeSpec
| TypeSig Field (Bind (TyVar, Embed TypeSpec) Sig)
-- { module f : Sig2, id . Sig1 } where Sig1 may use "id" to refer to Sig2
| SubmodSig Field (Bind (Ident, Embed SigExpr) Sig)
deriving (Show, Generic, Typeable)
data TypeSpec
=
-- abstract type definition: type f : *
AbstractTypeSpec Kind
-- manifest type alias: type f : * = t
| ManifestTypeSpec Kind Type
-- other ways of making types would also go here.
deriving (Show, Generic, Typeable)
-- SigExprs are the various sorts of things that a user can write in
-- places where we might want a signature. Actually there are only
-- two things: SigIdents of previously defined signatures, or literal
-- Sigs.
data SigExpr = SigLit Sig
| SigPath SigPath
deriving (Show, Generic, Typeable)
-- Section 4: Modules
-- A module is a sequence of definitions in the same way that a
-- signature is a sequence of specifications.
data Mod
=
NilMod
-- { val f : T = E, x . Mod} where Mod can refer to Expr by the name "x".
| ValMod Field (Bind (Var, Embed Type, Embed Expr) Mod)
-- { type f : * = T, a . Mod} within a module you have to define types,
-- can't just declare them abstractly.
| TypeMod Field (Bind (TyVar, Embed ManifestTypeDefn) Mod)
-- { module f = Mod2, id . Mod1 }
| SubmodMod Field (Bind (Ident, Embed ModExpr) Mod)
deriving (Show, Generic, Typeable)
data ManifestTypeDefn
= ManifestTypeDefn Kind Type
deriving (Show, Generic, Typeable)
-- Again the user can write various sort of things in places where they ought to write a module.
data ModExpr
=
-- path of a previously defined module
ModPath Path
-- literal module contents
| ModLit Mod
-- generative sealing of a module with a signature.
-- This is the principle means of data abstraction: by hiding the manfiest
-- definitions of some type components, new abstract types may be created.
| ModSeal ModExpr SigExpr
-- if I added functors, functor application would go here.
deriving (Show, Generic, Typeable)
-- Section 7 : Toplevel
-- stuff you can write in a file. Basically a sequence of signature
-- and module definitions.
data Toplevel
=
-- eof
TopNil
-- signature s = SigExpr ; ...
| TopSig (Bind (SigIdent, Embed SigExpr) Toplevel)
-- module m = ModExpr ; ...
| TopMod (Bind (Ident, Embed ModExpr) Toplevel)
deriving (Show, Generic, Typeable)
-- ====================
-- Example
example :: Toplevel
example = let
s2 = s2n "S2"
m1 = s2n "M1"
t = s2n "t"
mkTop top = top TopNil
mkSig si se = TopSig . bind (s2n si, embed se)
mkMod mi me = TopMod . bind (s2n mi, embed me)
seal m s = ModSeal m s
mkTS f Nothing = TypeSig f . bind (s2n f, embed (AbstractTypeSpec KType))
mkTS f (Just t') = TypeSig f . bind (s2n f, embed (ManifestTypeSpec KType t'))
mkTM f t' = TypeMod f . bind (s2n f, embed (ManifestTypeDefn KType t'))
sigLit se = SigLit (se NilSig)
modLit me = ModLit (me NilMod)
in
mkTop
$ mkSig "S1" (sigLit
$ mkTS "t" Nothing
. mkTS "s" (Just $ (TV t) `Arr` (TV t)))
. mkSig "S2" (sigLit
$ mkTS "t" Nothing)
. mkMod "M1" (modLit
$ mkTM "t" TInt
. mkTM "s" (TInt `Arr` (TV t)))
. mkMod "M2" (seal (ModPath $ Id m1) (SigPath $ SigIdent s2))
--
-- > typecheck example
-- Right ()
--
typecheck :: Toplevel -> Either String ()
typecheck top = runFreshM $ runExceptT $ runReaderT (checkToplevel top) ([], [])
-- ==========
-- Interlude - let's implement alpha-equivalence and substitution for everything.
instance Alpha Toplevel
instance Alpha SigExpr
instance Alpha SigPath
instance Alpha Sig
instance Alpha TypeSpec
instance Alpha ModExpr
instance Alpha Path
instance Alpha Mod
instance Alpha ManifestTypeDefn
instance Alpha TypePath
instance Alpha ValuePath
instance Alpha Kind
instance Alpha Type
instance Alpha Expr
instance Subst Path Path
instance Subst Path SigPath
instance Subst Path SigExpr
instance Subst Path Sig
instance Subst Path TypeSpec
instance Subst Path Mod
instance Subst Path ModExpr
instance Subst Path ManifestTypeDefn
instance Subst Path TypePath
instance Subst Path ValuePath
instance Subst Path Kind
instance Subst Path Type
instance Subst Path Expr
instance Subst Type Sig
instance Subst Type SigPath
instance Subst Type SigExpr
instance Subst Type TypeSpec
instance Subst Type Mod
instance Subst Type ModExpr
instance Subst Type ManifestTypeDefn
instance Subst Type Kind
instance Subst Type Type
instance Subst Type TypePath
instance Subst Type Path
instance Subst Type Expr
instance Subst Type ValuePath
-- ================================================================================
-- Part II: Typechecking
-- In general, in order to typecheck we will use two contexts that I
-- will write D and G. In D we will associate signature identifiers
-- with the signature that they stand for; module identifiers with the signature of that
-- module; and type variables with their type specs, where it's understood that bindings
-- that are added later may refer to everything in the context that comes earlier.
-- For example: module M : sig type t1 : * end ; type a : * = t1.
-- We will represent contexts as lists of bindings and we will cons onto the front of the list
-- when we add the latest bindings.
type DCtx = [DBinding]
data DBinding
=
-- signature S = sig ... end
DSig SigIdent Sig
-- module M : sig ... end
| DMod Ident Sig
-- type a : * or type a : * = t
| DType TyVar TypeSpec
-- The term context is used when typechecking value definitions and
-- expressions it's just a list of types for every variable that's in
-- scope.
type GCtx = [(Var, Type)]
-- To typecheck we need the contexts and a source of fresh names
type TC = ReaderT (DCtx, GCtx) (ExceptT String FreshM)
-- Let's go in reverse.
-- To check a toplevel we check the signature or module and extend the context and continue.
checkToplevel :: Toplevel -> TC ()
checkToplevel TopNil = return ()
checkToplevel (TopSig bnd) = do
((sigId, unembed -> sigExpr), rest) <- unbind bnd
sig <- checkSigExpr sigExpr
local (extendD $ DSig sigId sig) $ checkToplevel rest
checkToplevel (TopMod bnd) = do
((modId, unembed -> modExpr), rest) <- unbind bnd
sig <- checkModExpr modExpr
local (extendD $ DMod modId sig) $ checkToplevel rest
-- To check a SigExpr, lookup the sig ident in the context, or check
-- a literal sig field by field
checkSigExpr :: SigExpr -> TC Sig
checkSigExpr (SigPath (SigIdent sigId)) = lookupSigId sigId
checkSigExpr (SigLit sig) = do
checkSig sig
return sig
-- Check that Sig is well formed by going through the fields in turn.
checkSig :: Sig -> TC ()
checkSig NilSig = return ()
checkSig (ValSig _f t sig) = do
ensureType t KType -- t is the type of a value field, so it better have kind *
checkSig sig
checkSig (TypeSig _f bnd) = do
((tyVar, unembed -> spec), rest) <- unbind bnd
checkSpec spec
local (extendD $ DType tyVar spec) $ checkSig rest
checkSig (SubmodSig _f bnd) = do
((subId, unembed -> sigExpr), rest) <- unbind bnd
subSig <- checkSigExpr sigExpr
local (extendD $ DMod subId subSig) $ checkSig rest
-- check that a type spec is well-formed.
checkSpec :: TypeSpec -> TC ()
checkSpec (AbstractTypeSpec _k) = return ()
checkSpec (ManifestTypeSpec k t) = ensureType t k
kindOfTypeSpec :: TypeSpec -> Kind
kindOfTypeSpec spec =
case spec of
AbstractTypeSpec k -> k
ManifestTypeSpec k _ -> k
-- ensure that the given type is well formed and has a kind that is
-- equal to the given one.
ensureType :: Type -> Kind -> TC ()
ensureType t k = do
k' <- checkType t
unless (k `aeq` k')
$ throwError ("expected type " ++ show t
++ " to have kind " ++ show k
++ " but got " ++ show k')
-- check a module expression and return its natural signature. The
-- natural signature is the one you would read off from a literal
-- module. For a sealed module, its natural signature is the one that
-- is ascribed to it. For a module path its the embedding of its
-- strengthened signature into the Sig datatype (more on this
-- mysterious sentence later!)
checkModExpr :: ModExpr -> TC Sig
checkModExpr (ModLit modLit) = checkMod modLit
checkModExpr (ModSeal modExpr sigExpr) = do
naturalSig <- checkModExpr modExpr
-- check that the natural signature is at least as defined as the
-- sealing sig.
sealingSig <- checkSigExpr sigExpr
naturalSig `subSigOf` sealingSig
return sealingSig
checkModExpr (ModPath p) = do
strongSig <- lookupModulePath p
weakenStrong strongSig
-- check a module is well-formed and return its natural sig.
checkMod :: Mod -> TC Sig
checkMod NilMod = return NilSig
checkMod (ValMod f bnd) = do
((x, unembed -> ty, unembed -> e), rest) <- unbind bnd
checkExpr e ty
sigRest <- local (extendG $ (x, ty)) $ checkMod rest
return $ ValSig f ty sigRest
checkMod (TypeMod f bnd) = do
((tyVar, unembed -> manifestTypeDefn), rest) <- unbind bnd
spec <- checkManifestTypeDefn manifestTypeDefn
sigRest <- local (extendD $ DType tyVar spec) $ checkMod rest
return $ TypeSig f $ bind (tyVar, embed spec) sigRest
checkMod (SubmodMod f bnd) = do
((modId, unembed -> modExpr), rest) <- unbind bnd
subSig <- checkModExpr modExpr
sigRest <- local (extendD $ DMod modId subSig) $ checkMod rest
return $ SubmodSig f $ bind (modId, embed (SigLit subSig)) sigRest
checkManifestTypeDefn :: ManifestTypeDefn -> TC TypeSpec
checkManifestTypeDefn (ManifestTypeDefn k t) = do
ensureType t k
return $ ManifestTypeSpec k t
-- ==========
-- So now we know how to typecheck modules and signatures, except:
-- 1. I have yet to tell you how to typecheck expressions and
-- kindcheck types.
-- 2. Also these mysterious "Strong signatures" showed up.
-- 3. I need to write the implementation of 'subSigOf'
-- 4. Various utilities for manipulating contexts.
-- Let's start with the core language checking.
checkExpr :: Expr -> Type -> TC ()
checkExpr e t = do
-- In the language I showed so far, we can infer the type of every expression, so
-- checking is just running inference and then ensuring that the resulting type
-- is equivalent to the one we expected.
t' <- inferExpr e
isEq <- equivType t t'
unless isEq
$ throwError ("Expected the type of " ++ show e
++ " to be " ++ show t
++ " but got " ++ show t')
inferExpr :: Expr -> TC Type
inferExpr (V v) = lookupVar v
inferExpr (I _) = return TInt
inferExpr (App e1 e2) = do
tArr <- inferExpr e1
(tArg, tResult) <- ensureArrowTy tArr
checkExpr e2 tArg
return tResult
inferExpr (Lam bnd) = do
((x, unembed -> tArg), body) <- unbind bnd
ensureType tArg KType
tResult <- local (extendG (x, tArg)) $ inferExpr body
return (Arr tArg tResult)
inferExpr (P valuePath) = lookupValuePath valuePath
checkType :: Type -> TC Kind
checkType (TV tyVar) = do
spec <- lookupTyVar tyVar
return $ kindOfTypeSpec spec
checkType TInt = return KType
checkType (Arr t1 t2) = do
ensureType t1 KType
ensureType t2 KType
return KType
checkType (TP typePath) = kindOfTypeSpec <$> lookupTypePath typePath
ensureArrowTy :: Type -> TC (Type, Type)
ensureArrowTy t = do
t' <- expandAliases t
case t' of
Arr dom cod -> return (dom, cod)
_ -> throwError ("expected a function type, got " ++ show t)
equivType :: Type -> Type -> TC Bool
equivType t1 t2 = do
t1' <- expandAliases t1
t2' <- expandAliases t2
return (t1' `aeq` t2')
-- ====================
-- Okay, okay, let's talk about the strong signatures.
-- So the idea here is that when we go to look up a value path (for
-- example) assuming that all the fields along the path exist and
-- actually end up picking out a particular value field with some type
-- we want to return a type that shares as many type equalities as
-- possible with the previous definitions in the modules along the
-- path.
--
-- Example:
-- module M1 : {
-- type t1 = Int
-- a1 . module M2 : {
-- type t2 : *
-- a2 . type t3 = a1 -> a2
-- a3 . val x : a3
-- }
-- }
--
-- (recall that each type field tX also has an internal name aX by
-- which later components of its containing module refer to it)
--
-- Now if we see 'M1.M2.x' we want to return "Int -> M1.M2.t2" That
-- is, although the natural type of x is either "a3" or "M1.M2.t3"
-- depending on your perspective, that wouldn't expose as much sharing
-- as possible. (For example if there was a value y of type M1.t1 we
-- want to know that "x y" is a legal application -- that x has some
-- arrow type and that its domain is equivalent to the type of y).
--
-- So what we return instead is
-- {Int / a1} ({M1.M2.t2/a2} ({a1->a2 / a3} a3))
-- That is, as we traverse the module M1 to get to its M2
-- field, we substitute Int (the manifest rhs of t1) for a1 and
-- continue. Then when we descend into M2 and see that t2 is
-- abstract, we substitute for the internal name a2, the "selfified"
-- name M1.M2.t2. Finally when we go past t3, we replace a3 by the
-- rhs of the type alias, namely a1 -> a2 (which by now been transformed into Int -> M1.M2.t2).
-- An interesting property of carrying out this process to all of M1 is that dependencies among fields
-- disappear. Instead we end up with
-- module M1 : {
-- type t1 = Int
-- module M2 : {
-- type t2 : *
-- type t3 = Int -> M1.M2.t2
-- val x : Int -> M1.M2.t2
-- }
-- }
-- We will call this non-dependent sort of signature a "strengthened" (or selfified) signature.
-- It warrants its own datatype
data SelfSig
= NilSelfSig
| ValSelfSig Field Type SelfSig
| TypeSelfSig Field TypeSpec SelfSig
| SubmodSelfSig Field SelfSig SelfSig -- first SelfSig is the
-- selfified submodule, second
-- is the rest of this sig.
deriving Show
lookupModulePath :: Path -> TC SelfSig
lookupModulePath (Id modId) = do
weakSig <- lookupModuleId modId
strengthen (Id modId) weakSig
lookupModulePath (Project p f) = do
strongSig <- lookupModulePath p
projectModuleField strongSig f
lookupValuePath :: ValuePath -> TC Type
lookupValuePath (ValuePath p f) = do
strongSig <- lookupModulePath p
projectValueField strongSig f
lookupTypePath :: TypePath -> TC TypeSpec
lookupTypePath (TypePath p f) = do
strongSig <- lookupModulePath p
projectTypeField strongSig f
strengthen :: Path -> Sig -> TC SelfSig
strengthen _p NilSig = return NilSelfSig
strengthen p (ValSig f ty rest) = do
strongRest <- strengthen p rest
return (ValSelfSig f ty strongRest)
strengthen p (TypeSig f bnd) = do
((tyVar, unembed -> spec), rest) <- unbind bnd
let
self = TypePath p f
rest' = subst tyVar (TP self) rest
strongRest <- strengthen p rest'
return (TypeSelfSig f spec strongRest)
strengthen p (SubmodSig f bnd) = do
((subId, unembed -> subSigExpr), rest) <- unbind bnd
subSig <- checkSigExpr subSigExpr
let
self = Project p f
strongSub <- strengthen self subSig
let
rest' = subst subId self rest
strongRest <- strengthen p rest'
return (SubmodSelfSig f strongSub strongRest)
-- the reverse operation. Go from a SelfSig back to an ordinary Sig.
-- We need to pick some fresh names for the internal names of all the
-- components. we use the freshness monad to pick them. And of
-- course there won't be any references to them in the tail of the
-- signature because that's precisely the defining property of strong
-- sigs.
weakenStrong :: SelfSig -> TC Sig
weakenStrong NilSelfSig = return NilSig
weakenStrong (ValSelfSig f ty rest) = do
weakRest <- weakenStrong rest
return (ValSig f ty weakRest)
weakenStrong (TypeSelfSig f spec rest) = do
weakRest <- weakenStrong rest
tyvar <- fresh (hintFieldName f)
return $ TypeSig f $ bind (tyvar, embed spec) weakRest
weakenStrong (SubmodSelfSig f subSelfSig rest) = do
weakRest <- weakenStrong rest
weakSub <- weakenStrong subSelfSig
subId <- fresh (hintFieldName f)
return $ SubmodSig f $ bind (subId, embed $ SigLit weakSub) weakRest
-- make up a name (probably stale) from a given field.
hintFieldName :: Field -> Name a
hintFieldName = s2n
-- Given a strong signature, find its submodel field with the given
-- name and return that submodel's strong signature.
projectModuleField :: SelfSig -> Field -> TC SelfSig
projectModuleField NilSelfSig f =
throwError ("expected to find a submodule called " ++ f)
projectModuleField (ValSelfSig _ _ rest) f = projectModuleField rest f
projectModuleField (TypeSelfSig _ _ rest) f = projectModuleField rest f
projectModuleField (SubmodSelfSig f' subSig rest) f =
if f == f' then return subSig else projectModuleField rest f
projectTypeField :: SelfSig -> Field -> TC TypeSpec
projectTypeField NilSelfSig f =
throwError ("expected to find a type field called " ++ f)
projectTypeField (ValSelfSig _ _ rest) f = projectTypeField rest f
projectTypeField (TypeSelfSig f' spec rest) f =
if f == f' then return spec else projectTypeField rest f
projectTypeField (SubmodSelfSig _ _ rest) f = projectTypeField rest f
projectValueField :: SelfSig -> Field -> TC Type
projectValueField NilSelfSig f =
throwError ("expected to find a value field called " ++ f)
projectValueField (ValSelfSig f' ty rest) f =
if f == f' then return ty else projectValueField rest f
projectValueField (TypeSelfSig _ _ rest) f = projectValueField rest f
projectValueField (SubmodSelfSig _ _ rest) f = projectValueField rest f
-- ========================================
-- subsignature
subSigOf :: Sig -> Sig -> TC ()
subSigOf _sig1 _sig2 = return () -- tedious to implement
-- ===========================================================================
-- utilities
lookupModuleId :: Ident -> TC Sig
lookupModuleId modId = do
msig <- asks (findModule . fst)
case msig of
Just sig -> return sig
Nothing -> throwError ("no module " ++ show modId)
where
findModule [] = Nothing
findModule (DMod modId' sig : rest) =
if modId == modId' then Just sig else findModule rest
findModule (_ : rest) = findModule rest
lookupTyVar :: TyVar -> TC TypeSpec
lookupTyVar tv = do
mspec <- asks (findTyVar . fst)
case mspec of
Just spec -> return spec
Nothing -> throwError ("no type " ++ show tv)
where
findTyVar [] = Nothing
findTyVar (DType tv' spec : rest) =
if tv == tv' then Just spec else findTyVar rest
findTyVar (_ : rest) = findTyVar rest
lookupSigId :: SigIdent -> TC Sig
lookupSigId sigIdent = do
msig <- asks (findSig . fst)
case msig of
Just sig -> return sig
Nothing -> throwError ("no signature identifier " ++ show sigIdent)
where
findSig [] = Nothing
findSig (DSig sigIdent' sig : rest) =
if sigIdent == sigIdent' then Just sig else findSig rest
findSig (_ : rest) = findSig rest
lookupVar :: Var -> TC Type
lookupVar x = do
mt <- asks (Data.List.lookup x . snd)
case mt of
Just t -> return t
Nothing -> throwError ("no variable " ++ show x)
extendD :: DBinding -> (DCtx, GCtx) -> (DCtx, GCtx)
extendD b (d, g) = (b : d, g)
extendG :: (Var, Type) -> (DCtx, GCtx) -> (DCtx, GCtx)
extendG b (d, g) = (d, b:g)
--------------------
expandAliases :: Type -> TC Type
expandAliases (Arr t1 t2) = Arr <$> expandAliases t1 <*> expandAliases t2
expandAliases t@TInt = return t
expandAliases t@(TV a) = do
spec <- lookupTyVar a
case spec of
ManifestTypeSpec _ t' -> expandAliases t'
_ -> return t
expandAliases t@(TP p) = do
spec <- lookupTypePath p
case spec of
ManifestTypeSpec _ t' -> return t'
_ -> return t
@lambdageek
Copy link
Author

References

  1. Robert Harper and Mark Lillibridge. A type-theoretic approach to higher order modules with sharing. POPL 1994.
  2. Robert Harper and Chris Stone. A type-theoretic interpretation of Standard ML.
    In Proof, Language and Interaction: Essays in Honour of Robin Milner. The MIT
    Press, 2000. Extended version published as CMU technical report CMU-CS-97-147.
  3. Xavier Leroy. A modular module system. Journal of Functional Programming, Volume 10 Issue 3, May 2000.
  4. Stephanie Weirich, Brent A. Yorgey, and Tim Sheard. Binders Unbound. ICFP 2011.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment