Skip to content

Commit 2886458

Browse files
Geometer1729Geometer1729
committed
Polymorphic types
1 parent ba375b0 commit 2886458

File tree

5 files changed

+263
-73
lines changed

5 files changed

+263
-73
lines changed

‎src/DicePrelude.hs

+139-25
Original file line numberDiff line numberDiff line change
@@ -1,34 +1,148 @@
1+
{-# LANGUAGE AllowAmbiguousTypes #-}
2+
{-# LANGUAGE QuantifiedConstraints #-}
3+
14
module DicePrelude where
25

36
import Data.Map qualified as M
4-
import Data.Singletons (SingI)
5-
import TypeCheckerCore (DType (..), ExprT (Lit), HsOf, Res (Res))
6-
7-
class (HsOf (DOf l) ~ l, SingI (DOf l)) => Lit l where
8-
type DOf l :: DType
9-
lit :: l -> Res
10-
lit = Res @(DOf l) . lit'
11-
lit' :: l -> ExprT (DOf l)
12-
lit' = Lit
13-
14-
instance Lit Int where
15-
type DOf Int = DInt
16-
17-
instance Lit Bool where
18-
type DOf Bool = DBool
7+
import TypeCheckerCore (DType (..), ExprT (Hask), Res (Res), HRefable (..), Ref, sRef, HsOf)
8+
import Prelude.Singletons (withSingI)
9+
import Data.Singletons (SingI(..), Sing)
1910

20-
instance (Lit a, Lit b) => Lit (a -> b) where
21-
type DOf (a -> b) = DFun (DOf a) (DOf b)
2211

2312
prelude :: Map Text Res
2413
prelude =
2514
M.fromList
26-
[ ("+", lit @(Int -> _) (+))
27-
, ("-", lit @(Int -> _) (-))
28-
, ("*", lit @(Int -> _) (*))
29-
, ("/", lit @(Int -> _) div)
30-
, ("^", lit @(Int -> Int -> Int) (^))
31-
, ("**", lit @(Int -> Int -> Int) (^))
32-
, ("&&", lit @(Bool -> _) (&&))
33-
, ("||", lit @(Bool -> _) (&&))
15+
[ ("+", easy $ (+) @Int)
16+
, ("-", easy $ (-) @Int)
17+
, ("*", easy $ (*) @Int)
18+
, ("/", easy $ div @Int)
19+
, ("^", easy $ (^) @Int @Int)
20+
, ("**", easy $ (^) @Int @Int)
21+
, ("&&", easy (&&))
22+
, ("||", easy (||))
23+
-- TODO classes so you can compare lists and such?
24+
, (">", easy $ (>) @Int)
25+
, ("<", easy $ (<) @Int)
26+
, (">=", easy $ (>=) @Int)
27+
, ("<=", easy $ (<=) @Int)
28+
, ("==", easy $ (==) @Int)
29+
, ("/=", easy $ (/=) @Int)
30+
, ("++", easyP @([H0] -> [H0] -> [H0]) (++))
31+
, ("ifte", easyP @(Bool -> H0 -> H0 -> H0)
32+
(\c t f -> if c then t else f))
33+
, ("True" , easy True)
34+
, ("False" , easy False)
35+
, ("replicate" , easyP @(Int -> H0 -> [H0]) replicate)
36+
-- TODO probably better if this works more like replicateM
37+
-- may require seperate builtin?
38+
, ("even" , easy @(Int -> Bool) even)
39+
, ("odd" , easy @(Int -> Bool) odd)
40+
, ("id", easyP @(H0 -> H0) id)
41+
, ("length" , easyP @([H0] -> Int) length)
42+
, ("filter" , easyP @((H0 -> Bool) -> [H0] -> [H0]) filter)
43+
-- TODO more prelude functions
44+
-- especially (.)
3445
]
46+
47+
48+
easyP :: forall h.
49+
(SingI (DOf h) ,Just0 (DOf h)) => (forall d. HsOf (Ref 0 d (DOf h))) -> Res
50+
easyP h = Res @(DOf h) $ buildPoly @h (\(Proxy :: Proxy d) -> h @d)
51+
52+
buildPoly :: forall h . (SingI (DOf h) ,Just0 (DOf h)) =>
53+
(forall d. Proxy d -> HsOf (Ref 0 d (DOf h))) -> ExprT (DOf h)
54+
buildPoly h = Hask $ HRef p (h $ Proxy @(DVar 0))
55+
where
56+
p :: forall n t. (SingI n,SingI t) =>
57+
Proxy '(n,t) -> HRefable (Ref n t (DOf h))
58+
p Proxy = case sRef (sing @n) (sing @t) (sing @(DVar 0)) of
59+
(t' :: Sing t') -> withSingI t' $ case j01 @(DOf h) (Proxy @'(n,t)) of
60+
J01 -> go (Proxy @t')
61+
62+
go :: forall t. SingI t => Proxy t -> HRefable (Ref 0 t (DOf h))
63+
go Proxy = HRef
64+
(\(Proxy :: Proxy '(n1,t1)) -> case sRef (sing @n1) (sing @t1) (sing @t) of
65+
(t' :: Sing t') -> case j02 @(DOf h) (Proxy @'(n1,t,t1)) of
66+
J02 -> withSingI t' $ go (Proxy @t')
67+
)
68+
(h $ Proxy @t)
69+
70+
data HVar (n :: Natural) where
71+
type H0 = HVar 0
72+
type H1 = HVar 1
73+
74+
type DOf :: Type -> DType
75+
type family DOf (t :: Type) where
76+
DOf Int = DInt
77+
DOf Bool = DBool
78+
DOf [a] = DList (DOf a)
79+
DOf (a -> b) = DFun (DOf a) (DOf b)
80+
DOf (HVar n) = DVar n
81+
82+
-- Class for DTypes only polymorphic over DVar 0
83+
class Ref 0 (DVar 0) d ~ d => Just0 (d :: DType) where
84+
j01 :: Proxy '(n,t) -> Just0D1 n t d
85+
j02 :: Proxy '(n,t,t1) -> Just0D2 n t t1 d
86+
87+
data Just0D1 n t (d :: DType) where
88+
J01 :: Ref 0 (Ref n t (DVar 0)) d ~ Ref n t d => Just0D1 n t d
89+
90+
data Just0D2 n t1 t2 (d :: DType) where
91+
J02 :: Ref 0 (Ref n t2 t1) d ~ Ref n t2 (Ref 0 t1 d) => Just0D2 n t1 t2 d
92+
93+
instance Just0 (DVar 0) where
94+
j01 Proxy = J01
95+
j02 Proxy = J02
96+
97+
instance Just0 DInt where
98+
j01 Proxy = J01
99+
j02 Proxy = J02
100+
101+
instance Just0 DBool where
102+
j01 Proxy = J01
103+
j02 Proxy = J02
104+
105+
instance Just0 l => Just0 (DList l) where
106+
j01 p = case j01 @l p of
107+
J01 -> J01
108+
j02 p = case j02 @l p of
109+
J02 -> J02
110+
111+
instance (Just0 a,Just0 b) => Just0 (DFun a b) where
112+
j01 p = case j01 @a p of
113+
J01 -> case j01 @b p of
114+
J01 -> J01
115+
j02 p = case j02 @a p of
116+
J02 -> case j02 @b p of
117+
J02 -> J02
118+
119+
-- Constant under refs
120+
data CRef (d :: DType) (n :: Natural) (t :: DType) where
121+
CRef :: d ~ Ref n t d => CRef d n t
122+
123+
withCref :: forall d n t a. DEasy d => (Ref n t d ~ d => a) -> a
124+
withCref = case cref @d (Proxy @'(n,t)) of
125+
CRef -> id
126+
127+
class SingI d => DEasy (d :: DType) where
128+
cref :: Proxy '(n,t) -> CRef d n t
129+
easy' :: HsOf d -> ExprT d
130+
131+
easy :: forall h. (HsOf (DOf h) ~ h, DEasy (DOf h)) => h -> Res
132+
easy a = Res $ easy' @(DOf h) a
133+
134+
instance DEasy DInt where
135+
cref Proxy = CRef
136+
easy' n = let go = HRef (\Proxy -> go) n in Hask go
137+
138+
instance DEasy DBool where
139+
cref Proxy = CRef
140+
easy' n = let go = HRef (\Proxy -> go) n in Hask go
141+
142+
instance DEasy l => DEasy (DList l) where
143+
cref (Proxy :: Proxy '(n,t)) = withCref @l @n @t CRef
144+
easy' n = let go = HRef (\(Proxy :: Proxy '(n,t)) -> withCref @l @n @t go) n in Hask go
145+
146+
instance (DEasy a,DEasy b) => DEasy (DFun a b) where
147+
cref (Proxy :: Proxy '(n,t)) = withCref @a @n @t $ withCref @b @n @t $ CRef
148+
easy' n = let go = HRef (\(Proxy :: Proxy '(n,t)) -> withCref @a @n @t $ withCref @b @n @t go) n in Hask go

‎src/Parser.hs

+1-1
Original file line numberDiff line numberDiff line change
@@ -60,8 +60,8 @@ infixes = buildExpressionParser table apps
6060
where
6161
table =
6262
[ binary <$> ["++"]
63-
, binary <$> ["&&", "||"]
6463
, binary <$> ["<", "<=", "==", "/=", ">", ">="]
64+
, binary <$> ["&&", "||"]
6565
, binary <$> ["^", "**"]
6666
, binary <$> ["*", "/"]
6767
, binary <$> ["+", "-"]

‎src/RollM.hs

+3-3
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
module RollM (rollDice, RollM (..)) where
22

3-
import TypeCheckerCore (ExprT (..), HsOf)
3+
import TypeCheckerCore (ExprT (..), HsOf,DType(DVar), HRefable (..))
44

55
class (Monad m) => RollM m where
66
range :: Int -> Int -> m Int
@@ -15,9 +15,9 @@ class (Monad m) => RollM m where
1515
d :: (RollM r) => Int -> r Int
1616
d = range 1
1717

18-
rollDice :: (RollM r, HsOf d ~ t) => ExprT d -> r t
18+
rollDice :: forall r d t. (RollM r, HsOf d ~ t) => ExprT d -> r t
1919
rollDice = \case
20-
Lit l -> pure l
20+
Hask (HRef _ l) -> pure l
2121
App f x -> rollDice f <*> rollDice x
2222
Dice a b -> do
2323
a' <- rollDice a

‎src/TypeCheck.hs

+28-30
Original file line numberDiff line numberDiff line change
@@ -7,28 +7,11 @@ import DicePrelude (prelude)
77
import TypeCheckerCore
88

99
import Data.Map qualified as M
10-
import Data.Singletons (
11-
SingInstance (SingInstance),
12-
demote,
13-
fromSing,
14-
sing,
15-
singInstance,
16-
)
1710
import Data.Singletons.Decide (decideEquality, type (:~:) (Refl))
11+
import Prelude.Singletons
1812

1913
type Roll = ExprT DInt
2014

21-
testEval :: Res -> String
22-
testEval (Res (e :: ExprT d)) =
23-
case sing @d of
24-
SDInt -> show $ eval e
25-
_ -> "Test eval requires an int at top level"
26-
where
27-
eval :: ExprT (t :: DType) -> HsOf t
28-
eval (Lit l) = l
29-
eval (App f x) = eval f $ eval x
30-
eval (Dice _ _) = error "Test eval doesn't roll dice"
31-
3215
parseAndType :: Text -> Either Text Roll
3316
parseAndType expr = do
3417
r <- parseExpr $ toString expr
@@ -42,18 +25,8 @@ typeTopLevel e = case evalStateT (typeExpr e) 0 of
4225
bad -> Left $ "Top level dice expresions must be of type Int your expresion was of type " <> show (fromSing bad)
4326

4427
typeExpr :: Expr -> StateT Natural (Either Text) Res
45-
typeExpr (P.IntLit n) = lift $ Right $ Res @DInt (Lit $ fromInteger n)
46-
typeExpr (P.App f x) = do
47-
Res (fe :: ExprT ft) <- typeExpr f
48-
Res (xe :: ExprT xt) <- typeExpr x
49-
case sing @ft of
50-
SDFun @xt' @yt xt yt -> case decideEquality xt (sing @xt) of
51-
Nothing -> lift $ Left $ "Couldn't match " <> show (demote @xt) <> " with " <> show (fromSing xt)
52-
Just (Refl :: xt' :~: xt) ->
53-
-- Case brings SingI yt into scope
54-
case singInstance yt of
55-
SingInstance -> pure $ Res $ App fe xe
56-
_ -> lift $ Left "Applied argument to non-function. too many arguments?"
28+
typeExpr (P.IntLit n) = lift $ Right $ Res @DInt (Hask $ let go = HRef (const go) (fromInteger n) in go)
29+
-- TODO there will probably be a helper for this so use it here
5730
typeExpr (P.Paren e) = typeExpr e
5831
typeExpr (P.Infix name e1 e2) = typeExpr $ P.App (P.App (P.Var name) e1) e2
5932
typeExpr (P.IfTE e1 e2 e3) = typeExpr $ P.App (P.App (P.App (P.Var "ifte") e1) e2) e3
@@ -69,3 +42,28 @@ typeExpr (P.Dice l r) = do
6942
(SDInt, _) -> lift $ Left "number of faces must have type Int"
7043
(_, _) -> lift $ Left "number of dice must have type Int"
7144
typeExpr (P.Lambda _ _) = lift $ Left "Lambda functions are not implemented yet"
45+
typeExpr (P.App f x) = do
46+
Res (fe :: ExprT ft) <- typeExpr f
47+
Res (xe :: ExprT xt) <- typeExpr x
48+
case sing @ft of
49+
SDFun @xt' @yt xt' yt -> withSingI yt $
50+
case decideEquality xt' (sing @xt) of
51+
Just (Refl :: xt' :~: xt) ->
52+
pure $ Res $ App fe xe
53+
Nothing -> case sUnify xt' (sing @xt) of
54+
SNothing ->
55+
lift $ Left $ "Couldn't match type "
56+
<> show (demote @xt) <> " with "
57+
<> show (fromSing xt')
58+
SJust (refs :: Sing refs) -> withSingI xt' $ withSingI refs $ let
59+
fe' :: ExprT (DFun (Refine refs xt') (Refine refs yt)) =
60+
case funMaps @refs @xt' @yt of
61+
FunMaps -> refineExpr @refs fe
62+
xe' :: ExprT (Refine refs xt) = refineExpr @refs xe
63+
in case decideEquality (sRefine refs xt') (sRefine refs (sing @xt)) of
64+
Nothing -> lift $ Left "Type checker error, unify produced invalid refinements"
65+
Just Refl -> case singInstance (sRefine refs yt) of
66+
SingInstance -> pure $ Res $ App fe' xe'
67+
-- TODO This is actually wrong, it should suport unifications from vars to functions
68+
_ -> lift $ Left "Applied argument to non-function. too many arguments?"
69+

0 commit comments

Comments
 (0)