Skip to content

Instantly share code, notes, and snippets.

@chrisdone

chrisdone/0README.md

Last active May 9, 2020
Embed
What would you like to do?
Various type inference designs/sketches

Type Inference: Various Designs

I'm exploring the right data types for writing a type inference with higher kinds and poly types.

Putting more things in the type system can force you to think about more things, but it also can make it harder and more verbose to write and read algorithms.

-- This one implements a fairly good type inferer, with a free monad,
-- but kinds are not enforced, and forall/schemes are not considered atll.
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ApplicativeDo #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE LambdaCase #-}
-- |
--
-- 1. Produce skeletons for structure (-> for lambdas, int, etc.)
-- 3. Equality constraints t~t' are given as leftovers.
-- 2. Unknown types--type variables--are returned, too.
-- 3. Class constraints are bubbled up around each expression.
-- 4. Finally, we unify all the constraints.
-- 5. We resolve instances that are complete.
-- 6. We complain about class constraints that aren't filled in.
-- 7. Make sure that you can't define: id :: a -> a; id x = 6
-- <https://gitlab.haskell.org/ghc/ghc/issues/4499>
-- Note
--
-- It seems clear below that unknown and p0 can be unified (one-way;
-- rigids are like constants); i.e. all p0's become unknown's, same
-- for out/r2.
--
-- Elaboration would let me explicitly state this, as a kind of elab
-- :: [constraint] -> [constraint] that would yield further
-- constraints based on what we see here.
--
-- Furthermore, rigids are only relevant when checking the definition
-- of a toplevel or let with an explicit type signature. Otherwise;
-- they may also be relevant for using a name "read-only" without
-- changing its type-variables in-place to match our use; instead we
-- copy them. So f Int or f Char works fine.
--
--
-- Constraints:
-- p0 -> r3 ≡ p1
-- Int -> r2 ≡ r3
-- unknown -> (unknown -> Int -> out) -> out ≡ p0 -> p1 -> r2
--
-- unknown -> (unknown -> Int -> out) -> out -- from expression
module Duet.Infer2 where
import Control.Applicative.Free
import Control.Monad.Free
import Control.Monad.State
import Data.List
import Text.Printf
--------------------------------------------------------------------------------
-- Types
data T
= VT String -- variable
| CT String -- constant
| FT T T -- func
deriving (Eq)
instance Show T where
show = go False
where
go o =
\case
VT v -> v
CT s -> s
FT a b -> opt "(" ++ go True a ++ " -> " ++ go False b ++ opt ")"
where opt str =
if o
then str
else ""
--------------------------------------------------------------------------------
-- Expression
data E s
= CE T
| LE (SType s) String (E s)
| VE (SType s) String
| AE (SType s) (E s) (E s)
--------------------------------------------------------------------------------
-- Stages
data Stage = PreInfer | PostInfer
type family SType s where
SType 'PreInfer = Maybe T
SType 'PostInfer = T
--------------------------------------------------------------------------------
-- Inferer
inferE :: E 'PreInfer -> Infer (E 'PostInfer)
inferE = go
where
go =
\case
CE t -> pure (CE t)
LE msig p e -> do
pt <- liftStep (NewVT "p")
liftStep (BindTV p pt)
e' <- go e
let lt = FT pt (eType e')
lt' <-
case msig of
Nothing -> pure lt
Just t -> do
liftStep (Equiv t lt)
pure t
pure (LE lt' p e')
VE msig p -> do
mt <- liftStep (LookupP p)
case mt of
Nothing -> liftStep (MissingP p)
Just t ->
case msig of
Nothing -> pure (VE t p)
Just sigt -> do
liftStep (Equiv sigt t)
pure (VE sigt p)
AE msig f x -> do
rt <- liftStep (NewVT "r")
case msig of
Nothing -> pure ()
Just t -> liftStep (Equiv t rt)
f' <- go f
x' <- go x
let ft_expected = FT (eType x') rt
liftStep (Equiv ft_expected (eType f'))
pure (AE rt f' x')
--------------------------------------------------------------------------------
-- Infer monad
data InferStep a where
NewVT :: String -> InferStep T
BindTV :: String -> T -> InferStep ()
LookupP :: String -> InferStep (Maybe T)
MissingP :: String -> InferStep a
Equiv :: T -> T -> InferStep ()
newtype Infer a = Infer
{ unInfer :: Free (Ap InferStep) a
} deriving (Functor, Applicative, Monad)
liftStep :: InferStep a -> Infer a
liftStep = Infer . liftF . liftAp
data S = S
{ idents :: Int
, constraints :: [(T, T)]
, env :: [(String, T)]
, vars :: [T]
}
runInfer :: Infer (E 'PostInfer) -> (E 'PostInfer, S)
runInfer m =
runState
(foldFree (runAp reify) (unInfer m))
(S {idents = 0, constraints = [], env = [], vars = []})
where
reify :: InferStep a -> State S a
reify =
\case
NewVT prefix -> do
i <- gets idents
let t = (VT (prefix ++ show i))
modify (\s -> s {idents = i + 1, vars = vars s ++ [t]})
pure t
BindTV p t -> modify (\s -> s {env = (p, t) : (env s)})
LookupP p -> gets env >>= pure . lookup p
MissingP i -> error ("Missing parameter " ++ i)
Equiv x y ->
modify (\s -> s {constraints = (constraints s) ++ [(x, y)]})
--------------------------------------------------------------------------------
-- Debug
instance Show S where
show S {idents, constraints, env, vars} =
unlines
[ "Identifier counter: " ++ show idents
, "Environment:"
, unlines (map (\(p, t) -> p ++ " :: " ++ show t) env)
, unlines (map show vars)
, "Constraints:"
, tablize
(map
(\(t, t') -> [(False, show t), (False, ""), (True, show t')])
constraints)
]
debug example =
let (t, state) = runInfer (inferE example)
in do print t
print state
putStrLn (show (eType t) ++ " -- from expression")
{-putStrLn
(graph
(Left (eType t) :
map Left (vars state) ++ map Right (constraints state)))-}
graph :: [Either T (T,T)] -> String
graph cs = unlines ["strict digraph {", unlines (map go cs), "}"]
where
go (Left e) = unlines [show (show e) ++ ";", splice e]
go (Right (x, y)) =
unlines
[ unlines
[ unlines
[ show (show yt) ++ "->" ++ show (show xt) ++ " [dir=none, color=\"black:invis:black\"];"
]
| xt <- [x]
, yt <- [y]
]
, splice x
, splice y
]
splice x =
unlines
[show (show t) ++ "->" ++ show (show x) ++ ";" | t <- tVars x, t /= x]
tVars :: T -> [T]
tVars =
\case
FT x y -> concatMap tVars [x, y]
t -> [t]
-- | Make a table out of a list of rows.
tablize :: [[(Bool,String)]] -> String
tablize xs =
intercalate "\n"
(map (intercalate " " . map fill . zip [0 ..]) xs)
where fill (x',(left',text')) = printf ("%" ++ direction ++ show width ++ "s") text'
where direction = if left'
then "-"
else ""
width = maximum (map (length . snd . (!! x')) xs)
instance Show (E 'PreInfer) where
show = \case
CE t -> "(_ :: " ++ show t ++ ")"
LE t p e -> "(\\" ++ p ++ " -> " ++ show e ++ ")"
VE t v -> v
AE t f x -> "(" ++ show f ++ " " ++ show x ++ ")"
instance Show (E 'PostInfer) where
show = \case
CE t -> "(_ :: " ++ show t ++ ")"
LE t p e -> "((\\" ++ p ++ " -> " ++ show e ++ ") :: " ++ show t ++ ")"
VE t v -> "(" ++ v ++ " :: " ++ show t ++ ")"
AE t f x -> "((" ++ show f ++ " " ++ show x ++ ") :: " ++ show t ++ ")"
eType :: E 'PostInfer -> T
eType =
\case
CE t -> t
LE t _ _ -> t
VE t _ -> t
AE t _ _ -> t
example0 :: E 'PreInfer
example0 =
LE Nothing "f" (AE Nothing (VE Nothing "f") (CE (CT "Int")))
example1 :: E 'PreInfer
example1 =
LE
(Just
(FT
(RT "unknown")
(FT (FT (RT "unknown") (FT (CT "Int") (RT "out"))) (RT "out"))))
"x"
(LE
Nothing
"f"
(AE
Nothing
(AE Nothing (VE Nothing "f") (VE Nothing "x"))
(CE (CT "Int"))))
example2_wrong :: E 'PreInfer
example2_wrong =
LE Nothing "f" (AE Nothing (VE Nothing "f") (VE Nothing "f"))
-- This one separates the kind from the return @a@ value.
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase, StandaloneDeriving, GADTs #-}
data Type env k a where
-- Regular types
-- A constant type.
C :: Show k => k -> Type env k ()
-- A free variable.
Free :: Show k => k -> Type env k ()
-- App.
Ap :: Type env (i :-> k) () -> Type env i () -> Type env k ()
-- Schemes
-- This correponds to a rigid.
V :: Var env k t -> Type env k t
-- This corresponds to forall a. ... a ...
L :: Type (a,env) o b -> Type env (Forall i o) (a -> b)
-- This wouldn't be writable by a user.
A :: Type env (Forall k o) (a -> b) -> Type env k a -> Type env o b
deriving instance Show (Type env k a)
data Forall k o = Forall k o deriving (Show)
data TypeK = TypeK deriving (Show)
data a :-> k = a :-> k deriving (Show)
data Var env k t where
VZ :: Var (t, env) k t
VS :: Var env k t -> Var (a, env) k t
deriving instance Show (Var env k t)
eval :: env -> Type env k t -> t
eval _ Ap {} = ()
eval _ Free{} = ()
eval env (V v) = lookp v env
eval _ C{} = ()
eval env (L e) = \x -> eval (x, env) e
eval env (A e1 e2) = (eval env e1) (eval env e2)
lookp :: Var env k t -> env -> t
lookp VZ (x,_) = x
lookp (VS v) (_, env) = lookp v env
{-
Example:
> eval () (A (L (V VZ)) (C 'a'))
'a'
-- const
> eval () (A (A (L (L (V (VS VZ)))) (C 'a')) (C 123))
'a'
-}
-- This one pushes kinds and generic vars into the type system with a nested tuples approach.
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeOperators, LambdaCase, StandaloneDeriving, GADTs #-}
module StructuredInfer where
import Control.Applicative.Free
import Control.Monad.Free
import Control.Monad.State
import Data.List
import Data.Typeable
import Numeric.Natural
import Text.Printf
--------------------------------------------------------------------------------
-- Types
data Type env kind where
-- A constant type. Add kinds?
-- Maybe, (), Int, Either, (->), etc.
Constructor :: String -> kind -> Type env kind
-- A free variable.
-- a
FreeVariable :: Natural -> kind -> Type env kind
-- Type application.
-- Maybe a
Application :: (Show ki, Show ko) => Type env (ki -> ko) -> Type env ki -> Type env ko
-- A generic variable used in a forall scheme.
-- Rigid variables that will not unify with free variables.
GenericVariable :: (env ~ (t, env')) => Var env kind -> Type env kind
-- Forall scheme:
-- forall. a -> ... a ...
-- Forall :: (Show b, env' ~ (a,env)) => Type (x,env') b -> Type env' b
-- -- This wouldn't be writable by a user.
-- -- E.g. Show a => a -> String
-- -- Instantiate with: Int
-- -- Int -> String
-- InstantiateForall :: Type env (Forall a b) -> Type env a -> Type env b
-- -- Class qualification
-- -- E.g. Show a => a -> String
-- Qualify :: c -> Var env x -> Type env o -> Type env ((c, x) :=> o)
-- -- Row types.
-- -- E.g. { a :: Int, b :: String }
-- Row :: Row env -> Type env RowKind
data SchemeOrType env kind where
SchemeType :: SchemeOrType (a, env) kind -> SchemeOrType env kind
TypeType :: Type env kind -> SchemeOrType env kind
instance Show (SchemeOrType e k) where show _ = "s"
functionCons :: Type e (() -> () -> ())
functionCons = undefined {-Constructor "(->)" (TypeK :*-> (TypeK :*-> TypeK))-}
functionType :: Type e TypeK -> Type e TypeK -> Type e TypeK
functionType i o = undefined {-Application (Application functionCons i) o-}
instance Show (Type e k) where
show t0 = go 0 t0
where
go ::
forall e k. Int
-> Type e k
-> String
go nesting =
\case
Constructor str kind -> "" ++ str ++ "" -- " :: " ++ show kind ++
FreeVariable nat kind -> "v" ++ show nat ++ "" -- ++ " :: " ++ show kind
Application (Application (Constructor "(->)" _) x) y ->
"(" ++ go nesting x ++ " -> " ++ go nesting y ++ ")"
Application typeF typeX ->
"(" ++ show typeF ++ " " ++ indent (show typeX) ++ ")"
-- Forall t ->
-- "(forall _" ++ show nesting ++ ". " ++ go (nesting + 1) t ++ ")"
GenericVariable var -> "_" ++ show (varnesting var)
varnesting :: Var env t -> Int
varnesting =
\case
VZ -> 0
VS v -> 1 + varnesting v
indent :: String -> String
indent = intercalate "\n" . map (" " ++) . lines
--------------------------------------------------------------------------------
-- Kinds
data Kind a where
TypeK :: Kind ()
(:*->) :: Kind a -> Kind b -> Kind (a -> b)
instance Show (Kind a) where show _ = "Kind"
type TypeK = Kind ()
--------------------------------------------------------------------------------
-- Vars
data Var env t where
VZ :: Var (t, env) t
VS :: Var env t -> Var (a, env) t
deriving instance Show (Var env t)
--------------------------------------------------------------------------------
-- Expression
data E s
= CE (SomeKindedType TypeK) -- this needs to be an arbitrary thing
| LE (SType s (Type () TypeK)) Natural (E s)
| VE (SType s (Type () TypeK)) Natural
| AE (SType s (Type () TypeK)) (E s) (E s)
eType :: E 'PostInfer -> SomeKindedType TypeK
eType =
\case
CE t -> t
LE t _ _ -> SomeKindedType (TypeType t)
VE t _ -> SomeKindedType (TypeType t)
AE t _ _ -> SomeKindedType (TypeType t)
instance Show (E 'PreInfer) where
show = \case
CE t -> "(_ :: " ++ show t ++ ")"
LE t p e -> "(\\p" ++ show p ++ " -> " ++ show e ++ ")"
VE t v -> "p"++ show v
AE t f x -> "(" ++ show f ++ " " ++ show x ++ ")"
instance Show (E 'PostInfer) where
show = \case
CE t -> "(_ :: " ++ show t ++ ")"
LE t p e -> "((\\p" ++ show p ++ " -> " ++ show e ++ ") :: " ++ show t ++ ")"
VE t v -> "(p" ++ show v ++ " :: " ++ show t ++ ")"
AE t f x -> "((" ++ show f ++ " " ++ show x ++ ") :: " ++ show t ++ ")"
--------------------------------------------------------------------------------
-- Stages
data Stage = PreInfer | PostInfer
type family SType s t where
SType 'PreInfer t = Maybe t
SType 'PostInfer t = t
--------------------------------------------------------------------------------
-- Infer algebra
data InferStep a where
NewVT :: (Typeable env, Typeable k, Show k) => k -> InferStep (Type env k)
BindTV :: (Typeable env) => Natural -> Type env TypeK -> InferStep ()
LookupP :: Natural -> InferStep (SomeKindedType TypeK)
Equiv :: (Show k) => Type env k -> Type env k -> InferStep ()
deriving instance Show (InferStep a)
data SomeKindedType k =
forall env. (Typeable env) =>
SomeKindedType (SchemeOrType env k)
deriving instance Show k => Show (SomeKindedType k)
--------------------------------------------------------------------------------
-- Inferer
-- TODO:
--
-- We need to distinguish between
--
-- * /Defining/ an expression whose type is forall'd (make sure types are polymorphic)
-- * /Using/ a variable whose type is forall'd (instantiate scheme with fresh variables)
--
-- And make sure that this situation makes sense (this is a case of /using/):
--
-- (Int -> v3) ≡ v0 <--- this is a lambda parameter,
-- (Char -> v4) ≡ v0 <--- presenty we don't know its type because
--- we don't provide a sig for the param,
--- nor do we figure it out based on the
--- lambda's type (we could)
-- (v4 -> v1) ≡ v2
-- (v3 -> v2) ≡ (forall _0. (_0 -> (forall _1. (_1 -> ()))))
-- ((forall _0. (_0 -> _0)) -> ()) ≡ (v0 -> v1)
inferE :: E 'PreInfer -> Infer (E 'PostInfer)
inferE = go
where
go =
\case
CE t -> pure (CE t)
LE msig p e -> do
pt <- liftStep (NewVT TypeK)
liftStep (BindTV p pt)
e' <- go e
let lt = functionType pt (undefined (eType e'))
lt' <-
case msig of
Nothing -> pure lt
Just t -> do
liftStep (Equiv t lt)
pure t
pure (LE lt' p e')
VE msig p -> do
sky <- liftStep (LookupP p)
t <- instantiate sky
case msig of
Nothing -> pure (VE t p)
Just sigt -> do
liftStep (Equiv sigt t)
pure (VE sigt p)
AE msig f x -> do
rt <- liftStep (NewVT TypeK)
case msig of
Nothing -> pure ()
Just t -> liftStep (Equiv t rt)
f' <- go f
x' <- go x
let ft_expected = functionType (undefined (eType x')) rt
liftStep (Equiv ft_expected (undefined (eType f')))
pure (AE rt f' x')
instantiate :: SomeKindedType TypeK -> Infer (Type () TypeK)
instantiate (SomeKindedType schemeOrType) = go schemeOrType
where go =
\case
SchemeType t -> undefined
eval :: e -> Type e k -> k
eval e =
\case
Constructor s k -> k
FreeVariable s k -> k
Application s k -> (eval e s) (eval e k)
-- Forall inner -> pure (\x -> eval (x, e) inner)
GenericVariable var -> (lookp var e)
lookp :: Var env t -> env -> t
lookp VZ (x,_) = x
lookp (VS v) (_, env) = lookp v env
--------------------------------------------------------------------------------
-- Infer monad
newtype Infer a = Infer
{ unInfer :: Free (Ap InferStep) a
} deriving (Functor, Applicative, Monad)
liftStep :: InferStep a -> Infer a
liftStep = Infer . liftF . liftAp
--------------------------------------------------------------------------------
-- Infer monad runner
data SomeEquivalence =
forall env k. (Show k) =>
SomeEquivalence (Type env k, Type env k)
data SomeType =
forall env k. (Typeable k, Typeable env, Show k) =>
SomeType (Type env k)
deriving instance Show SomeType
data S = S
{ idents :: !Natural
, constraints :: ![SomeEquivalence]
, env :: ![(Natural, SomeKindedType TypeK)]
, vars :: ![SomeType]
}
runInfer :: Infer (E 'PostInfer) -> IO (E 'PostInfer, S)
runInfer m =
runStateT
(foldFree (runAp (printit >=> reify)) (unInfer m))
(S {idents = 0, constraints = [], env = [], vars = []})
where
printit x = x <$ lift (print x)
reify :: InferStep a -> StateT S IO a
reify =
\case
NewVT kind -> do
nat <- gets idents
let t = (FreeVariable nat kind)
modify (\s -> s {idents = nat + 1, vars = vars s ++ [SomeType t]})
pure t
BindTV p t -> modify (\s -> s {env = (p, SomeKindedType (TypeType t)) : (env s)})
LookupP p -> do
r <- gets env >>= pure . lookup p
case r of
Nothing -> error "variable not in scope!"
Just yes -> pure yes
Equiv x y ->
modify
(\s -> s {constraints = (constraints s) ++ [SomeEquivalence (x, y)]})
instance Show S where
show S {idents, constraints, env, vars} =
unlines
[ "Identifier counter: " ++ show idents
, "Environment:"
, unlines (map (\(p, t) -> show p ++ " :: " ++ show t) env)
, unlines (map show vars)
, "Constraints:"
, tablize
(map
(\(SomeEquivalence (t, t')) -> [(False, show t), (False, ""), (True, show t')])
constraints)
]
debug :: (Show (E 'PostInfer)) => E 'PreInfer -> IO ()
debug example = do
(t, s) <- runInfer (inferE example)
print example
putStrLn "=>"
print t
print s
putStrLn (show (eType t) ++ " -- from expression")
tablize :: (Foldable t, PrintfArg (t a)) => [[(Bool, t a)]] -> [Char]
tablize xs =
intercalate "\n"
(map (intercalate " " . map fill . zip [0 ..]) xs)
where fill (x',(left',text')) = printf ("%" ++ direction ++ show width ++ "s") text'
where direction = if left'
then "-"
else ""
width = maximum (map (length . snd . (!! x')) xs)
example0 :: E 'PreInfer
example0 =
LE Nothing 0 (AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType (Constructor "Int" TypeK :: Type () TypeK)))))
example1_err :: E 'PreInfer
example1_err =
LE Nothing 0 (AE Nothing (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))) (VE Nothing 0))
example2_err :: E 'PreInfer
example2_err =
LE
Nothing {-(Just (functionType (GenericVariable VZ) (GenericVariable VZ)))-}
0
(AE Nothing (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))) (VE Nothing 0))
example3_correct :: E 'PreInfer
example3_correct =
LE
Nothing
{-(Just (Forall (functionType (functionType (Constructor "Int" TypeK) (GenericVariable VZ)) (GenericVariable VZ))))-}
0
(AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))))
example3_err :: E 'PreInfer
example3_err =
LE
Nothing{-(Just (Forall (functionType (functionType (GenericVariable VZ) (GenericVariable VZ)) (GenericVariable VZ))))-}
0
(AE Nothing (VE Nothing 0) (CE (SomeKindedType(TypeType(Constructor "Int" TypeK :: Type () TypeK)))))
example4_ok :: E 'PreInfer
example4_ok =
LE
Nothing
{-(Just
(functionType
(Forall (functionType (GenericVariable VZ) (GenericVariable VZ)))
(Constructor "()" TypeK)))-}
0
(AE
Nothing
(AE
Nothing
(CE
(SomeKindedType @(TypeK) @(TypeK, (TypeK, ()))
(SchemeType
(SchemeType
(TypeType
(functionType
(GenericVariable VZ)
(functionType
(GenericVariable (VS VZ))
(Constructor "()" TypeK))))))))
(AE
Nothing
(VE Nothing 0)
(CE
(SomeKindedType
(TypeType (Constructor "Int" TypeK :: Type () TypeK))))))
(AE
Nothing
(VE Nothing 0)
(CE
(SomeKindedType
(TypeType (Constructor "Char" TypeK :: Type () TypeK))))))
-- This one borrows from Oleg's typed eval, but doesn't actually implement any hard things yet.
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE LambdaCase, StandaloneDeriving, GADTs #-}
data a :-> b = a :-> b
data a :=> b = a :=> b
data Type env t where
-- A constant type. Add kinds?
C :: a -> Type env a
-- This correponds to a rigid.
V :: Var env t -> Type env t
-- This corresponds to forall. a -> ... a ...
L :: Type (a,env) b -> Type env (a-> b)
-- This wouldn't be writable by a user.
A :: Type env (a-> b) -> Type env a -> Type env b
-- A free variable.
Free :: Type env ()
-- An a -> b type.
Fun :: Type env a -> Type env b -> Type env (a :-> b)
-- Class qualification: C x => a
Qual :: c -> Var env x -> Type env o -> Type env ((c, x) :=> o)
data Var env t where
VZ :: Var (t, env) t
VS :: Var env t -> Var (a, env) t
deriving instance Show (Var env t)
eval :: env -> Type env t -> t
eval env (Qual c v t) = (c, lookp v env) :=> eval env t
eval _ Free = ()
eval env (V v) = lookp v env
eval _ (C c) = c
eval env (L e) = \x -> eval (x, env) e
eval env (A e1 e2) = (eval env e1) (eval env e2)
eval env (Fun x y) = eval env x :-> eval env y
lookp :: Var env t -> env -> t
lookp VZ (x,_) = x
lookp (VS v) (_, env) = lookp v env
{-
Example:
> eval () (A (L (V VZ)) (C 'a'))
'a'
-- const
> eval () (A (A (L (L (V (VS VZ)))) (C 'a')) (C 123))
'a'
-}
-- This one pushes kinds into the type system and also generic vars.
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE GADTs #-}
module InferV3 where
import Data.Finite
import GHC.TypeLits
data Monomorphic
data Polymorphic (n :: Nat)
data a :-> b = a :-> b deriving Show; infixr 2 :->
data Type s k where
Var :: Integer -> k -> Type s k
Con :: String -> k -> Type s k
App :: Type s (i :-> o) -> Type s i -> Type s o
-- We use a @Finite@ to ensure that any @Gen@ instance is always
-- within the bounds of the @forall x y z. ...@ -- this is a
-- Polymorphic 3.
--
-- We could even go as far as to use @Polymorphic 0@ to mean "not
-- polymorphic", but I'm not sure how I feel about that.
Gen :: Finite n -> k -> Type (Polymorphic n) k
-- If the @Finite@ and Nat in the @Polymorphic@ doesn't work out, we
-- can just drop it.
data SomePolyType k =
forall n. KnownNat n =>
SomePolyType (Type (Polymorphic n) k)
-- | Convert a polymorphic type to a monomorphic type.
--
-- In other words, replace all the @Gen@ with @Var@.
mono :: SomePolyType k -> (Type Monomorphic k)
mono (SomePolyType t) = go t
where go :: Type (Polymorphic n) k -> Type Monomorphic k
go =
\case
-- Here we lookup, or if missing, generate. The function
-- @genToVar idx k@ should always be idempotent. It should also
-- check that the returned lookup variable has the same kind;
-- else that's an error.
Gen idx k -> undefined
--
Var idx k -> Var idx k
Con s k -> Con s k
App f x -> App (go f) (go x)
-- | Generalize a monomorphic type to a polymorphic type.
poly :: Type Monomorphic k -> SomePolyType k
poly = undefined
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.