dunham/newt
1
0
Fork 0
Code Issues Pull Requests Actions 1 Packages Projects Releases Wiki Activity

Typeclass works for Monad

Browse Source
This commit is contained in:
Steve Dunham
2024-10-29 16:35:34 -07:00
parent d96e23d954
commit 0fb5b08598
9 changed files with 120 additions and 153 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
TODO.md
View File

@@ -1,21 +1,13 @@
## TODO
NOW - two things
1. I broke Tree.newt by removing some over-aggressive reduction. I need to
make it happen during unification. Not sure if I have all of the bits to vappspine there.
2. Need to collect constraints and re-run, I think that may get me to
typeclasses
- [x] Remember operators from imports
- [ ] Default cases for non-primitives (currently gets expanded to all constructors)
- [x] Case for primitives
- [ ] aoc2023 translation
- [x] day1
- [x] day2
- some "real world" examples
- some "real world" examples -v
- [x] Maybe Eq and stuff would work for typeclass without dealing with unification issues yet
- [x] unsolved meta errors repeat (need to freeze or only report at end)
- [x] Sanitize JS idents, e.g. `_+_`
@@ -46,12 +38,7 @@ typeclasses
- Agda doesn't have it, clashes with pair syntax
- [ ] autos / typeclass resolution
- [x] very primitive version in place, not higher order, search at end
- We need special handling in unification to make this possible for typeclasses on `U -> U`, we could still do `Eq` or `Show` with the current unification
- options
- keep as implicit and do auto if the type constructor is flagged auto
- keep as implicit and mark auto, behavior overlaps a lot with implicit
- have separate type of implict with `{{}}`
- `TypeClass.newt` is the exercise for this
- [x] monad is now working
- [ ] do blocks (needs typeclass, overloaded functions, or constrain to IO)
- [x] some solution for `+` problem (classes? ambiguity?)
- [x] show compiler failure in the editor (exit code != 0)
@@ -67,7 +54,7 @@ typeclasses
- I think we got this by not switching for single cases
- [ ] magic nat (codegen as number with appropriate pattern matching)
- [ ] magic tuple? (codegen as array)
- [ ] magic newtype? (drop in codegen)
- [ ] magic newtype? (drop them in codegen)
- [ ] records / copatterns
- [x] vscode: syntax highlighting for String
- [ ] add `pop` or variant of `pfunc` that maps to an operator, giving the js operator and precedence on RHS

59
newt/TypeClass.newt
View File

@@ -1,17 +1,5 @@
module TypeClass
-- experiment on one option for typeclass (we don't have record yet)
-- this would be nicer with records and copatterns
-- At this point, for Agda style, I'll probably need to postpone, or collect constraints
-- at lesat. Idris style, I might get away without short term.
-- So I can read mcbride paper and maybe agda source.
-- we need a bit more than this, but
data Monad : (U -> U) -> U where
MkMonad : { M : U -> U } ->
(bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
@@ -21,7 +9,6 @@ data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B
Right : {A B : U} -> B -> Either A B
@@ -37,14 +24,9 @@ bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a
-- I think it was picking up the Maybe before I made it less aggressive about eval
MaybeMonad : Monad Maybe
MaybeMonad = MkMonad bindMaybe
-- So the idea here is to have some implicits that are solved by search
-- Error here is from foo, with a bad FC. I think it might be showing up during search.
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {a} {b} {m} {{MkMonad bind'}} ma amb = bind' {a} {b} ma amb
@@ -52,46 +34,5 @@ infixl 1 _>>=_
ptype Int
-- It's bailing on MaybeMonad and picking up Either?
foo : Int -> Maybe Int
foo x = (Just x) >>= (\ x => Just 10)
-- NOW
-- Older notes below, but this is _close_, we're doing something like agda, and we're getting the right solution
-- It's over-expanded, and there is an unsolved meta that I think the solution would unlock. (Need to collect and
-- retry constraints)
-- *SOLVE meta 6 sp [< (%var 0 [< ]), (%meta 4 [< (%var 0 [< ])])] val (%ref Maybe [< (%meta 9 [< (%var 0 [< ]), (%var 1 [< ])])])
-- Essentially (m6 v0) (m4 ...) == Maybe Int and (m6 v0) (m2 v0) == Maybe Int
-- Idris gets this by specially treating determining arguments of an auto as "invertible". It then unifies
-- the last arg on each side and tries the rest, which is now in the pattern fragment.
-- Agda may do this slightly differently from Idris:
-- https://agda.readthedocs.io/en/v2.6.0.1/language/instance-arguments.html#instance-resolution
-- I think it searches, pulls in all possibilities and tries to unify them into place.
-- We'll want to extend our example to what I have in Foo2.agda to test that it finds the right
-- one. Maybe look at the source to see if there is any invertible trickery going on?
-- I know that here, if I fill in the instance, everything works out, so finding the instance that works
-- out might be sufficient. That might mean that a instance constraint is a pile of options that get
-- winnowed down?
-- Putting MaybeMonad in there helps the unification
-- of Maybe Int =?= ?m6 ?m2 (as Monad Maybe (the type) gives ?m6 is Maybe)
-- and MaybeEither would fail after a couple of steps. But it seems expensive/complex
-- to have to run the process down for each candidate.
-- Agda seems complicated, minting fresh metas for bits of potential solutions (which
-- may be tossed if the solution is ruled out.)
-- ^
/-
So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case
-/

2
src/Lib/CompileExp.idr
View File

@@ -93,7 +93,7 @@ compileTerm tm@(App _ _ _) with (funArgs tm)
-- apply (CRef "Meta\{show k}") args' [<] 0
arity <- case meta of
-- maybe throw
(Unsolved x j ctx _ _) => pure 0 -- FIXME # of Bound in ctx.bds
(Unsolved x j ctx _ _ _) => pure 0 -- FIXME # of Bound in ctx.bds
(Solved j tm) => pure $ getArity !(quote 0 tm)
apply (CRef "Meta\{show k}") args' [<] arity
_ | (t@(Ref fc nm _), args) = do

64
src/Lib/Elab.idr
View File

@@ -9,6 +9,7 @@ import Lib.Prettier
import Data.List
import Data.Vect
import Data.String
import Data.IORef
import Lib.Types
import Lib.Eval
import Lib.TopContext
@@ -53,7 +54,7 @@ lookupDef ctx name = go 0 ctx.types ctx.env
export
forceMeta : Val -> M Val
forceMeta (VMeta fc ix sp) = case !(lookupMeta ix) of
(Unsolved pos k xs _ _) => pure (VMeta fc ix sp)
(Unsolved pos k xs _ _ _) => pure (VMeta fc ix sp)
(Solved k t) => vappSpine t sp >>= forceMeta
forceMeta x = pure x
@@ -70,7 +71,7 @@ tryEval k sp =
-- Force far enough to compare types
forceType : Val -> M Val
forceType (VMeta fc ix sp) = case !(lookupMeta ix) of
(Unsolved x k xs _ _) => pure (VMeta fc ix sp)
(Unsolved x k xs _ _ _) => pure (VMeta fc ix sp)
(Solved k t) => vappSpine t sp >>= forceType
forceType x@(VRef fc nm _ sp) = fromMaybe x <$> tryEval nm sp
forceType x = pure x
@@ -87,6 +88,30 @@ Semigroup UnifyResult where
Monoid UnifyResult where
neutral = MkResult []
-- We need to switch to SortedMap here
export
updateMeta : Context -> Nat -> (MetaEntry -> M MetaEntry) -> M ()
updateMeta ctx ix f = do
mc <- readIORef ctx.metas
metas <- go mc.metas
writeIORef ctx.metas $ {metas := metas} mc
where
go : List MetaEntry -> M (List MetaEntry)
go [] = error' "Meta \{show ix} not found"
go (x@((Unsolved y k z w v ys)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs
go (x@((Solved k y)) :: xs) = if k == ix then (::xs) <$> f x else (x ::) <$> go xs
export
addConstraint : Context -> Nat -> SnocList Val -> Val -> M ()
addConstraint ctx ix sp tm = do
mc <- readIORef ctx.metas
updateMeta ctx ix $ \case
(Unsolved pos k a b c cons) => do
info (getFC tm) "Add constraint m\{show ix} \{show sp} =?= \{show tm}"
pure (Unsolved pos k a b c (MkMc (getFC tm) ctx sp tm :: cons))
(Solved k tm) => error' "Meta \{show k} already solved"
pure ()
parameters (ctx: Context)
-- return renaming, the position is the new VVar
invert : Nat -> SnocList Val -> M (List Nat)
@@ -140,27 +165,50 @@ parameters (ctx: Context)
-- REVIEW can I get better names in here?
lams (S k) tm = Lam emptyFC "arg_\{show k}" (lams k tm)
export
unify : (l : Nat) -> Val -> Val -> M UnifyResult
export
solve : (lvl : Nat) -> (k : Nat) -> SnocList Val -> Val -> M ()
solve l m sp t = do
meta@(Unsolved metaFC ix ctx ty kind) <- lookupMeta m
meta@(Unsolved metaFC ix ctx ty kind cons) <- lookupMeta m
| _ => error (getFC t) "Meta \{show m} already solved!"
debug "SOLVE \{show m} \{show kind} lvl \{show l} sp \{show sp} is \{show t}"
let size = length $ filter (\x => x == Bound) $ toList ctx.bds
debug "\{show m} size is \{show size}"
if (length sp /= size) then do
debug "\{show m} size is \{show size} sps \{show $ length sp}"
let True = length sp == size
| _ => do
-- need INFO that works like debug.
-- FIXME we probably need to hold onto the constraint and recheck when we solve the meta?
info (getFC t) "meta \{show m} (\{show ix}) applied to \{show $ length sp} args instead of \{show size}"
debug "CONSTRAINT m\{show ix} \{show sp} =?= \{show t}"
-- error (getFC t) "meta \{show m} applied to \{show $ length sp} args instead of \{show size}"
else do
-- add constraint to meta m
-- we can keep a list and run them when it is solved.
addConstraint ctx m sp t
debug "meta \{show meta}"
ren <- invert l sp
tm <- rename m ren l t
let tm = lams (length sp) tm
top <- get
soln <- eval [] CBN tm
solveMeta top m soln
updateMeta ctx m $ \case
(Unsolved pos k _ _ _ cons) => do
putStrLn "INFO at \{show pos}: solve \{show k} as \{pprint [] !(quote 0 soln)}"
pure $ Solved k soln
(Solved k x) => error' "Meta \{show ix} already solved!"
-- We're not breaking anything, but not quite getting an answer?
for_ cons $ \case
MkMc fc ctx sp rhs => do
val <- vappSpine soln sp
debug "discharge l=\{show ctx.lvl} \{(show val)} =?= \{(show rhs)}"
-- is this the right depth?
unify ctx.lvl val rhs
pure ()
trySolve : Nat -> Nat -> SnocList Val -> Val -> M ()
@@ -170,8 +218,6 @@ parameters (ctx: Context)
pure ())
export
unify : (l : Nat) -> Val -> Val -> M UnifyResult
unifySpine : Nat -> Bool -> SnocList Val -> SnocList Val -> M UnifyResult
unifySpine l False _ _ = error emptyFC "unify failed at head" -- unreachable now

32
src/Lib/Eval.idr
View File

@@ -79,7 +79,7 @@ eval env mode (App _ t u) = vapp !(eval env mode t) !(eval env mode u)
eval env mode (U fc) = pure (VU fc)
eval env mode (Meta fc i) =
case !(lookupMeta i) of
(Unsolved _ k xs _ _) => pure $ VMeta fc i [<]
(Unsolved _ k xs _ _ _) => pure $ VMeta fc i [<]
(Solved k t) => pure $ t
eval env mode (Lam fc x t) = pure $ VLam fc x (MkClosure env t)
eval env mode (Pi fc x icit a b) = pure $ VPi fc x icit !(eval env mode a) (MkClosure env b)
@@ -112,7 +112,7 @@ quote l (VVar fc k sp) = if k < l
else ?borken
quote l (VMeta fc i sp) =
case !(lookupMeta i) of
(Unsolved _ k xs _ _) => quoteSp l (Meta fc i) sp
(Unsolved _ k xs _ _ _) => quoteSp l (Meta fc i) sp
(Solved k t) => quote l !(vappSpine t sp)
quote l (VLam fc x t) = pure $ Lam fc x !(quote (S l) !(t $$ VVar emptyFC l [<]))
quote l (VPi fc x icit a b) = pure $ Pi fc x icit !(quote l a) !(quote (S l) !(b $$ VVar emptyFC l [<]))
@@ -128,35 +128,10 @@ export
nf : Env -> Tm -> M Tm
nf env t = quote (length env) !(eval env CBN t)
export
prval : Val -> M String
prval v = pure $ pprint [] !(quote 0 v)
export
prvalCtx : {auto ctx : Context} -> Val -> M String
prvalCtx v = pure $ pprint (toList $ map fst ctx.types) !(quote ctx.lvl v)
export
solveMeta : TopContext -> Nat -> Val -> M ()
solveMeta ctx ix tm = do
mc <- readIORef ctx.metas
metas <- go mc.metas [<]
writeIORef ctx.metas $ {metas := metas} mc
where
go : List MetaEntry -> SnocList MetaEntry -> M (List MetaEntry)
go [] _ = error' "Meta \{show ix} not found"
go (meta@(Unsolved pos k _ _ _) :: xs) lhs = if k == ix
then do
-- empty context should be ok, because this needs to be closed
putStrLn "INFO at \{show pos}: solve \{show k} as \{!(prval tm)}"
pure $ lhs <>> (Solved k tm :: xs)
else go xs (lhs :< meta)
go (meta@(Solved k _) :: xs) lhs = if k == ix
then error' "Meta \{show ix} already solved!"
else go xs (lhs :< meta)
-- REVIEW - might be easier if we inserted the meta without a bunch of explicit App
-- I believe Kovacs is doing that.
@@ -183,6 +158,7 @@ appSpine : Tm -> List Tm -> Tm
appSpine t [] = t
appSpine t (x :: xs) = appSpine (App (getFC t) t x) xs
-- TODO replace this with a variant on nf
zonkApp : TopContext -> Nat -> Env -> Tm -> List Tm -> M Tm
zonkApp top l env (App fc t u) sp = zonkApp top l env t (!(zonk top l env u) :: sp)
zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
@@ -192,7 +168,7 @@ zonkApp top l env t@(Meta fc k) sp = case !(lookupMeta k) of
foo <- vappSpine v ([<] <>< sp')
debug "-> result is \{show foo}"
quote l foo
(Unsolved x j xs _ _) => pure $ appSpine t sp
(Unsolved x j xs _ _ _) => pure $ appSpine t sp
zonkApp top l env t sp = pure $ appSpine !(zonk top l env t) sp
zonkAlt : TopContext -> Nat -> Env -> CaseAlt -> M CaseAlt

26
src/Lib/ProcessDecl.idr
View File

@@ -25,7 +25,7 @@ isCandidate _ _ = False
-- This is a crude first pass
-- TODO consider ctx
findMatches : Val -> List TopEntry -> M (List Tm)
findMatches : Val -> List TopEntry -> M (List (Tm, MetaContext))
findMatches ty [] = pure []
findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do
let True = isCandidate ty type | False => findMatches ty xs
@@ -38,10 +38,12 @@ findMatches ty ((MkEntry name type def@(Fn t)) :: xs) = do
-- TODO sort out the FC here
let fc = getFC ty
debug "TRY \{name} : \{pprint [] type} for \{show ty}"
-- This check is solving metas, so we save mc below in case we want this solution
tm <- check (mkCtx top.metas fc) (RVar fc name) ty
debug "Found \{pprint [] tm} for \{show ty}"
mc' <- readIORef top.metas
writeIORef top.metas mc
(tm ::) <$> findMatches ty xs)
((tm, mc') ::) <$> findMatches ty xs)
(\ err => do
debug "No match \{show ty} \{pprint [] type} \{showError "" err}"
writeIORef top.metas mc
@@ -127,14 +129,16 @@ processDecl (Def fc nm clauses) = do
mc <- readIORef top.metas
let mlen = length mc.metas `minus` mstart
-- FIXME every time we hit solve in this loop, we need to start over with mc.metas
for_ (take mlen mc.metas) $ \case
(Unsolved fc k ctx ty AutoSolve) => do
debug "auto solving \{show k} : \{show ty}"
(Unsolved fc k ctx ty AutoSolve _) => do
debug "AUTO solving \{show k} : \{show ty}"
-- we want the context here too.
[tm] <- findMatches ty top.defs
| res => error fc "Failed to solve \{show ty}, matches: \{show $ map (pprint []) res}"
[(tm,mc)] <- findMatches ty top.defs
| res => error fc "FAILED to solve \{show ty}, matches: \{show $ map (pprint [] . fst) res}"
writeIORef top.metas mc
val <- eval ctx.env CBN tm
debug "solution \{pprint [] tm} evaled to \{show val}"
debug "SOLUTION \{pprint [] tm} evaled to \{show val}"
let sp = makeSpine ctx.lvl ctx.bds
solve ctx ctx.lvl k sp val
pure ()
@@ -146,13 +150,15 @@ processDecl (Def fc nm clauses) = do
mc <- readIORef top.metas
for_ (take mlen mc.metas) $ \case
(Solved k x) => pure ()
(Unsolved (l,c) k ctx ty User) => do
(Unsolved (l,c) k ctx ty User cons) => do
-- TODO print here instead of during Elab
pure ()
(Unsolved (l,c) k ctx ty kind) => do
(Unsolved (l,c) k ctx ty kind cons) => do
tm <- quote ctx.lvl !(forceMeta ty)
-- Now that we're collecting errors, maybe we simply check at the end
addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm}"
-- TODO - log constraints?
addError $ E (l,c) "Unsolved meta \{show k} \{show kind} type \{pprint (names ctx) tm} \{show $ length cons} constraints"
debug "Add def \{nm} \{pprint [] tm'} : \{pprint [] ty}"
modify $ setDef nm ty (Fn tm')

13
src/Lib/Types.idr
View File

@@ -325,8 +325,12 @@ Show MetaKind where
show User = "User"
show AutoSolve = "Auto"
-- constrain meta applied to val to be a val
public export
data MetaEntry = Unsolved FC Nat Context Val MetaKind | Solved Nat Val
data MConstraint = MkMc FC Context (SnocList Val) Val
public export
data MetaEntry = Unsolved FC Nat Context Val MetaKind (List MConstraint) | Solved Nat Val
public export
@@ -399,6 +403,7 @@ record Context where
metas : IORef MetaContext
fc : FC
%name Context ctx
||| add a binding to environment
export
@@ -416,7 +421,7 @@ define ctx name val ty =
export
covering
Show MetaEntry where
show (Unsolved pos k ctx ty kind) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds}"
show (Unsolved pos k ctx ty kind constraints) = "Unsolved \{show pos} \{show k} \{show kind} : \{show ty} \{show ctx.bds} cs \{show $ length constraints}"
show (Solved k x) = "Solved \{show k} \{show x}"
export withPos : Context -> FC -> Context
@@ -447,7 +452,7 @@ freshMeta : Context -> FC -> Val -> MetaKind -> M Tm
freshMeta ctx fc ty kind = do
mc <- readIORef ctx.metas
putStrLn "INFO at \{show fc}: fresh meta \{show mc.next} : \{show ty}"
writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind ::) } mc
writeIORef ctx.metas $ { next $= S, metas $= (Unsolved fc mc.next ctx ty kind [] ::) } mc
pure $ applyBDs 0 (Meta emptyFC mc.next) ctx.bds
where
-- hope I got the right order here :)
@@ -471,7 +476,7 @@ lookupMeta ix = do
where
go : List MetaEntry -> M MetaEntry
go [] = error' "Meta \{show ix} not found"
go (meta@(Unsolved _ k ys _ _) :: xs) = if k == ix then pure meta else go xs
go (meta@(Unsolved _ k ys _ _ _) :: xs) = if k == ix then pure meta else go xs
go (meta@(Solved k x) :: xs) = if k == ix then pure meta else go xs
-- we need more of topcontext later - Maybe switch it up so we're not passing

3
tests/black/Tree.newt
View File

@@ -91,9 +91,6 @@ insert (intv x lx xu) (node2 y tly tyu) = case cmp x y of
inr tyu' => inr (node2 y tly tyu')
insert (intv x lx xu) (node3 y z tly tyz tzu) = case cmp x y of
inl xy => case insert (intv {_} {N y} x lx xy) tly of
-- TODO Here a meta is applied to an extra argument, if we ignore that
-- constraint we get a better one later - _but_ we probably need to check
-- the constraint later.
inl (v ** (tlv , tvy)) => inl (y ** (node2 v tlv tvy, node2 z tyz tzu))
inr tly' => inr (node3 y z tly' tyz tzu)
inr yx => case cmp x z of

37
tests/black/TypeClass.newt
View File

@@ -1,8 +1,5 @@
module TypeClass
-- experiment on one option for typeclass (we don't have record yet)
-- we need a bit more than this, but
data Monad : (U -> U) -> U where
MkMonad : { M : U -> U } ->
(bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
@@ -12,18 +9,30 @@ data Maybe : U -> U where
Just : {A : U} -> A -> Maybe A
Nothing : {A : U} -> Maybe A
data Either : U -> U -> U where
Left : {A B : U} -> A -> Either A B
Right : {A B : U} -> B -> Either A B
-- NEXT trying to get this to work. An equivalence is not found in pattern
-- matching
bindEither : {A B C : U} -> (Either A B) -> (B -> Either A C) -> Either A C
bindEither (Left a) amb = Left a
bindEither (Right b) amb = amb b
EitherMonad : {A : U} -> Monad (Either A)
EitherMonad = MkMonad {Either A} bindEither
bindMaybe : {A B : U} -> Maybe A -> (A -> Maybe B) -> Maybe B
bindMaybe Nothing amb = Nothing
bindMaybe (Just a) amb = amb a
-- [instance]
MaybeMonad : Monad Maybe
-- Agda case lambda might be nice..
-- The {Maybe} isn't solved in type for the case
MaybeMonad = MkMonad {Maybe} (\ {A} ma amb =>
case ma of
Nothing => Nothing
-- It doesn't discover pat$5 is A during pattern matching
-- oh, but var 0 value is var5
Just a => amb a)
MaybeMonad = MkMonad bindMaybe
_>>=_ : {a b : U} -> {m : U -> U} -> {{x : Monad m}} -> (m a) -> (a -> m b) -> m b
_>>=_ {a} {b} {m} {{MkMonad bind'}} ma amb = bind' {a} {b} ma amb
infixl 1 _>>=_
ptype Int
foo : Int -> Maybe Int
foo x = (Just x) >>= (\ x => Just 10)