First pass at sugar for instances.

Makefile

@@ -1,6 +1,9 @@
 SRCS=$(shell find src -name "*.idr")
 
-all: build/exec/newt build/exec/newt.js build/exec/newt.min.js
+.PHONY:
+
+all: build/exec/newt build/exec/newt.js
+# build/exec/newt.min.js
 
 build/exec/newt: ${SRCS}
 	idris2 --build newt.ipkg
@@ -17,3 +20,5 @@ test: build/exec/newt
 vscode:
 	cd newt-vscode && vsce package && code --install-extension *.vsix
 
+playground: .PHONY
+	cd playground && ./build

TODO.md

@@ -1,8 +1,11 @@
 
 ## TODO
 
+NOW - sorting out instance sugar for `Monad {a} -> (Either a)`.
+
 - [ ] accepting DCon for another type (skipping case, but should be an error)
 - [ ] don't allow (or dot) duplicate names on LHS
+- [ ] remove metas from context, M has TopContext
 - [ ] improve test driver
   - maybe a file listing jobs, whether they are known broken, optional expected output, optional expected JS execution output.
 - [x] forall / ∀ sugar (Maybe drop this, issues with `.` and `{A}` works fine)

playground/samples/Tour.newt

@@ -56,8 +56,9 @@ plus' = \ n m => case n of
     Z => m
     S n => S (plus' n m)
 
--- We can define operators, currently only infix
--- and we allow unicode and letters in operators
+-- We can define operators. Mixfix is supported, but we don't
+-- allow ambiguity (so you can't have both [_] and [_,_]). See
+-- the Reasoning.newt sample for a mixfix example.
 infixl 2 _≡_
 
 -- Here is an equality, like Idris, everything goes to the right of the colon
@@ -70,29 +71,18 @@ data _≡_ : {A : U} -> A -> A -> U where
 test : plus (S Z) (S Z) ≡ S (S Z)
 test = Refl
 
--- Ok now we do typeclasses.  There isn't any sugar, but we have
--- search for implicits marked with double brackets.
+-- Ok now we do typeclasses. `class` and `instance` are sugar for
+-- ordinary data and functions:
 
 -- Let's say we want a generic `_+_` operator
 infixl 7 _+_
 
--- We don't have records yet, so we define a single constructor
--- inductive type. Here we also use `∀ A.` which is sugar for `{A : _} ->`
-data Plus : U -> U where
-  MkPlus : ∀ A. (A -> A -> A) -> Plus A
+class Add a where
+  _+_ : a -> a -> a
 
--- and the generic function that uses it
--- the double brackets indicate an argument that is solved by search
-_+_ : ∀ A. {{_ : Plus A}} -> A -> A -> A
-_+_ {{MkPlus f}} x y = f x y
-
--- The typeclass is now defined, search will look for functions in scope
--- that return a type matching (same type constructor) the implicit
--- and only have implicit arguments (inspired by Agda).
-
--- We make an instance `Plus Nat`
-PlusNat : Plus Nat
-PlusNat = MkPlus plus
+instance Add Nat where
+  Z + m = m
+  (S n) + m = S (n + m)
 
 -- and it now finds the implicits, you'll see the solutions to the
 -- implicits if you hover over the `+`.
@@ -108,7 +98,7 @@ foo a b = ?
 -- javascript output. It is not doing erasure (or inlining) yet, so the
 -- code is a little verbose.
 
--- We can define native types:
+-- We can define native types, if the type is left off, it defaults to U
 
 ptype Int : U
 ptype String : U
@@ -133,36 +123,49 @@ pfunc plusString : String -> String -> String := "(x,y) => x + y"
 
 -- We can make them Plus instances:
 
-PlusInt : Plus Int
-PlusInt = MkPlus plusInt
 
-PlusString : Plus String
-PlusString = MkPlus plusString
+instance Add Int where
+  _+_ = plusInt
+
+instance Add String where
+  _+_ = plusString
 
 concat : String -> String -> String
 concat a b = a + b
 
 -- Now we define Monad
+class Monad (m : U -> U) where
+  pure : {a} -> a -> m a
+  bind : {a b} -> m a -> (a -> m b) -> m b
 
-data Monad : (U -> U) -> U where
+/-
+This desugars to:
+
+data Monad : (m : U -> U) -> U where
   MkMonad : {m : U -> U} ->
-            ({a : U} -> a -> m a) ->
-            ({a b : U} -> m a -> (a -> m b) -> m b) ->
+            (pure : {a : _} -> a -> m a) ->
+            (bind : {a : _} -> {b : _} -> m a -> a -> m b -> m b) ->
             Monad m
 
-pure : ∀ m. {{Monad m}} -> {a : U} -> a -> m a
-pure {{MkMonad p _}} a = p a
+pure : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> a -> m a
+pure {m} {{MkMonad pure bind}} = pure
+
+bind : {m : U -> U} -> {{_ : Monad m}} -> {a : _} -> {b : _} -> m a -> a -> m b -> m b
+bind {m} {{MkMonad pure bind}} = bind
+
+-/
 
 -- we can declare multiple infix operators at once
 infixl 1 _>>=_ _>>_
 
-_>>=_ : ∀ m a b. {{Monad m}} -> m a -> (a -> m b) -> m b
-_>>=_ {{MkMonad _ b}} ma amb = b ma amb
+_>>=_ : {m} {{Monad m}} {a b} -> m a -> (a -> m b) -> m b
+_>>=_ ma amb = bind ma amb
 
-_>>_ :  ∀ m a b. {{Monad m}} -> m a -> m b -> m b
+_>>_ :  {m} {{Monad m}} {a b} -> m a -> m b -> m b
 ma >> mb = ma >>= (λ _ => mb)
 
--- That's our Monad typeclass, now let's make a List monad
+-- Now we define list and show it is a monad. At the moment, I don't
+-- have sugar for Lists,
 
 infixr 3 _::_
 data List : U -> U where
@@ -174,15 +177,26 @@ _++_ : ∀ a.  List a -> List a -> List a
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-bindList : ∀ a b. List a -> (a -> List b) -> List b
-bindList Nil f = Nil
-bindList (x :: xs) f = f x ++ bindList xs f
+instance Monad List where
+  pure a = a :: Nil
+  bind Nil f = Nil
+  bind (x :: xs) f = f x ++ bind xs f
 
--- Both `\` and `λ` work for lambda expressions:
-MonadList : Monad List
-MonadList = MkMonad (λ a => a :: Nil) bindList
+/-
+This desugars to: (the names in guillemots are not user-accessible)
 
--- We'll want Pair below too.  `,` has been left for use as an operator.
+«Monad List,pure» : { a : U } -> a:0 -> List a:1
+pure a = _::_ a Nil
+
+«Monad List,bind» : { a : U } -> { b : U } -> (List a) -> (a -> List b) -> List b
+bind Nil f = Nil bind (_::_ x xs) f = _++_ (f x) (bind xs f)
+
+«Monad List» : Monad List
+«Monad List» = MkMonad «Monad List,pure» «Monad List,bind»
+
+-/
+
+-- We'll want Pair below.  `,` has been left for use as an operator.
 -- Also we see that → can be used in lieu of ->
 infixr 1 _,_ _×_
 data _×_ : U → U → U where

playground/samples/TypeClass.newt

@@ -1,42 +1,35 @@
 module TypeClass
 
-data Monad : (U -> U) -> U where
-  MkMonad : { M : U -> U } ->
-            (bind : {A B : U} -> (M A) -> (A -> M B) -> M B) ->
-            (pure : ∀ A. A -> M A) ->
-            Monad M
+class Monad (m : U → U) where
+  bind : {a b} → m a → (a → m b) → m b
+  pure : {a} → a → m a
 
 infixl 1 _>>=_ _>>_
-_>>=_ : ∀ m a b. {{Monad m}} -> (m a) -> (a -> m b) -> m b
-_>>=_ {{MkMonad bind' _}}  ma amb = bind' ma amb
+_>>=_ : {m} {{Monad m}} {a b} -> (m a) -> (a -> m b) -> m b
+ma >>= amb = bind ma amb
 
 _>>_ : ∀ m a b. {{Monad m}} -> m a -> m b -> m b
 ma >> mb = mb
 
-pure : ∀ m a. {{Monad m}} -> a -> m a
-pure {{MkMonad _ pure'}} a = pure' a
-
 data Either : U -> U -> U where
   Left : ∀ A B. A -> Either A B
   Right : ∀ A B. B -> Either A B
 
-bindEither : ∀ A B C. (Either A B) -> (B -> Either A C) -> Either A C
-bindEither (Left a) amb = Left a
-bindEither (Right b) amb = amb b
+instance {a} → Monad (Either a) where
+  bind (Left a) amb = Left a
+  bind (Right b) amb = amb b
 
-EitherMonad : ∀ A. Monad (Either A)
-EitherMonad = MkMonad {Either A} bindEither Right
+  pure a = Right a
 
 data Maybe : U -> U where
   Just    : ∀ A. A -> Maybe A
   Nothing : ∀ A. Maybe A
 
-bindMaybe : ∀ A B. Maybe A -> (A -> Maybe B) -> Maybe B
-bindMaybe Nothing amb = Nothing
-bindMaybe (Just a) amb = amb a
+instance Monad Maybe where
+  bind Nothing amb = Nothing
+  bind (Just a) amb = amb a
 
-MaybeMonad : Monad Maybe
-MaybeMonad = MkMonad bindMaybe Just
+  pure a = Just a
 
 infixr 7 _::_
 data List : U -> U where
@@ -48,16 +41,11 @@ _++_ : ∀ A. List A -> List A -> List A
 Nil ++ ys = ys
 (x :: xs) ++ ys = x :: (xs ++ ys)
 
-bindList : ∀ A B. List A -> (A -> List B) -> List B
-bindList Nil f = Nil
-bindList (x :: xs) f = f x ++ bindList xs f
+instance Monad List where
+  bind Nil f = Nil
+  bind (x :: xs) f = f x ++ bind xs f
 
-singleton : ∀ A. A -> List A
-singleton a = a :: Nil
-
--- TODO need better error when the monad is not defined
-ListMonad : Monad List
-ListMonad = MkMonad bindList singleton
+  pure x = x :: Nil
 
 infixr 1 _,_
 data Pair : U -> U -> U where

src/Lib/Eval.idr

@@ -157,7 +157,7 @@ eval env mode (Let fc nm t u) = pure $ VLet fc nm !(eval env mode t) !(eval (VVa
 -- translate to a level
 eval env mode (Bnd fc i) = case getAt i env of
   Just rval => pure rval
-  Nothing => error' "Bad deBruin index \{show i}"
+  Nothing => error fc "Bad deBruin index \{show i}"
 eval env mode (Lit fc lit) = pure $ VLit fc lit
 
 eval env mode tm@(Case fc sc alts) = do

src/Lib/Parser.idr

@@ -406,7 +406,7 @@ parseData = do
 nakedBind : Parser Telescope
 nakedBind = do
   names <- some (withPos varname)
-  pure $ map (\(pos,name) => (pos, name, Implicit,  RImplicit pos)) names
+  pure $ map (\(pos,name) => (pos, name, Explicit,  RImplicit pos)) names
 
 export
 parseClass : Parser Decl
@@ -419,6 +419,16 @@ parseClass = do
   decls <- startBlock $ manySame $ parseSig
   pure $ Class fc name (join teles) decls
 
+export
+parseInstance : Parser Decl
+parseInstance = do
+  fc <- getPos
+  keyword "instance"
+  ty <- typeExpr
+  keyword "where"
+  decls <- startBlock $ manySame $ parseDef
+  pure $ Instance fc ty decls
+
 -- Not sure what I want here.
 -- I can't get a Tm without a type, and then we're covered by the other stuff
 parseNorm : Parser Decl
@@ -427,7 +437,8 @@ parseNorm = DCheck <$> getPos <* keyword "#check" <*> typeExpr <* keyword ":" <*
 export
 parseDecl : Parser Decl
 parseDecl = parseMixfix <|> parsePType <|> parsePFunc
-  <|> parseNorm <|> parseData <|> parseSig <|> parseDef <|> parseClass
+  <|> parseNorm <|> parseData <|> parseSig <|> parseDef
+  <|> parseClass <|> parseInstance
 
 
 export

src/Lib/ProcessDecl.idr

@@ -3,6 +3,7 @@ module Lib.ProcessDecl
 import Data.IORef
 import Data.String
 import Data.Vect
+import Data.List
 import Data.Maybe
 
 import Lib.Elab
@@ -27,7 +28,7 @@ isCandidate _ _ = False
 -- TODO consider ctx
 findMatches : Context -> Val -> List TopEntry -> M (List (Tm, MetaContext))
 findMatches ctx ty [] = pure []
-findMatches ctx ty ((MkEntry name type def@(Fn t)) :: xs) = do
+findMatches ctx ty ((MkEntry name type def) :: xs) = do
   let True = isCandidate ty type | False => findMatches ctx ty xs
   top <- get
   -- let ctx = mkCtx top.metas (getFC ty)
@@ -207,8 +208,10 @@ processDecl (Def fc nm clauses) = do
 
   putStrLn "check \{nm} at \{pprint [] ty}"
   vty <- eval empty CBN ty
+
   debug "\{nm} vty is \{show vty}"
 
+
   -- I can take LHS apart syntactically or elaborate it with an infer
   clauses' <- traverse (makeClause top) clauses
   tm <- buildTree (mkCtx top.metas fc) (MkProb clauses' vty)
@@ -217,7 +220,6 @@ processDecl (Def fc nm clauses) = do
   mc <- readIORef top.metas
   let mlen = length mc.metas `minus` mstart
   solveAutos mlen (take mlen mc.metas)
-
   -- TODO - make nf that expands all metas and drop zonk
   -- Day1.newt is a test case
   -- tm' <- nf [] tm
@@ -261,16 +263,14 @@ processDecl (Class classFC nm tele decls) = do
   processDecl decl
   for_ fields $ \ (fc,name,ty) => do
       let funType = teleToPi impTele $ RPi fc Nothing Auto tail ty
-
-      putStrLn "\{name} : \{pretty funType}"
-      processDecl $ TypeSig fc [name] funType
-
       let autoPat = foldl (\acc, (fc,nm,ty) => RApp fc acc (RVar fc nm) Explicit) (RVar classFC dcName) fields
-      putStrLn "\{pretty autoPat}"
       let lhs = foldl (\acc, (fc', nm, _, _) => RApp fc' acc (RVar fc' nm) Implicit) (RVar fc name) tele
       let lhs = RApp classFC lhs autoPat Auto
       let decl = Def fc name [(lhs, (RVar fc name))]
+
+      putStrLn "\{name} : \{pretty funType}"
       putStrLn "\{pretty decl}"
+      processDecl $ TypeSig fc [name] funType
       processDecl decl
   where
 
@@ -287,6 +287,99 @@ processDecl (Class classFC nm tele decls) = do
     teleToPi [] end = end
     teleToPi ((fc, nm, icit, ty) :: tele) end = RPi fc (Just nm) icit ty (teleToPi tele end)
 
+processDecl (Instance instfc ty decls) = do
+  let decls = collectDecl decls
+  putStrLn "-----"
+  putStrLn "Instance \{pretty ty}"
+  top <- get
+  let tyFC = getFC ty
+
+  vty <- check (mkCtx top.metas instfc) ty (VU instfc)
+  -- Here `tele` holds arguments to the instance
+  let (codomain, tele) = splitTele vty
+  -- env represents the environment of those arguments
+  let env = tenv (length tele)
+  debug "codomain \{pprint [] codomain}"
+  debug "tele is \{show tele}"
+
+  -- ok so we need a name, a hack for now.
+  -- Maybe we need to ask the user (e.g. `instance someName : Monad Foo where`)
+  -- or use "Monad\{show $ length defs}"
+  let instname = interpolate $ pprint [] codomain
+  let sigDecl = TypeSig instfc [instname] ty
+
+  let (Ref _ tconName _, args) := funArgs codomain
+    | (tm, _) => error tyFC "\{pprint [] codomain} doesn't appear to be a TCon application"
+  let (Just (MkEntry name type (TCon cons))) = lookup tconName top
+    | _ => error tyFC "\{tconName} is not a type constructor"
+  let [con] = cons
+    | _ => error tyFC "\{tconName} has multiple constructors \{show cons}"
+  let (Just (MkEntry _ dcty (DCon _ _))) = lookup con top
+    | _ => error tyFC "can't find constructor \{show con}"
+  vdcty@(VPi _ nm icit a b) <- eval [] CBN dcty
+    | x => error (getFC x) "dcty not Pi"
+  debug "dcty \{pprint [] dcty}"
+  let (_,args) = funArgs codomain
+
+  debug "traverse \{show $ map showTm args}"
+  -- This is a little painful because we're reverse engineering the
+  -- individual types back out from the composite type
+  args' <- traverse (eval env CBN) args
+  debug "args' is \{show args'}"
+  conTele <- getFields !(apply vdcty args') env []
+  -- declare individual functions, collect their defs
+  defs <- for conTele $ \case
+     (MkBind fc nm Explicit ty) => do
+       let ty' = foldr (\(MkBind fc nm' icit ty'), acc => Pi fc nm' icit ty' acc) ty tele
+       let nm' = "\{instname},\{nm}"
+       -- we're working with a Tm, so we define directly instead of processDecl
+       setDef nm' fc ty' Axiom
+       let Just (Def fc name xs) = find (\case (Def y name xs) => name == nm; _ => False) decls
+          | _ => error instfc "no definition for \{nm}"
+
+       let decl = (Def fc nm' xs)
+       putStrLn "***"
+       putStrLn "«\{nm'}» : \{pprint [] ty'}"
+       putStrLn $ render 80 $ pretty decl
+       pure $ Just decl
+     _ => pure Nothing
+  -- This needs to be declared before processing the defs, but the defs need to be
+  -- declared before this
+  processDecl sigDecl
+  for_ (mapMaybe id defs) $ \decl => do
+    -- debug because already printed above, but nice to have it near processing
+    debug $ render 80 $ pretty decl
+    processDecl decl
+
+  let decl = Def instfc instname [(RVar instfc instname, mkRHS instname conTele (RVar instfc con))]
+  putStrLn "SIGDECL"
+  putStrLn "\{pretty sigDecl}"
+  putStrLn $ render 80 $ pretty decl
+  processDecl decl
+  where
+    -- try to extract types of individual fields from the typeclass dcon
+    -- We're assuming they don't depend on each other.
+    getFields : Val -> Env -> List Binder -> M (List Binder)
+    getFields tm@(VPi fc nm Explicit ty sc) env bnds = do
+      bnd <- MkBind fc nm Explicit <$> quote (length env) ty
+      getFields !(sc $$ VVar fc (length env) [<]) env (bnd :: bnds)
+    getFields tm@(VPi fc nm _ ty sc) env bnds = getFields !(sc $$ VVar fc (length env) [<]) env bnds
+    getFields tm xs bnds = pure $ reverse bnds
+
+    tenv : Nat -> Env
+    tenv Z = []
+    tenv (S k) = (VVar emptyFC k [<] :: tenv k)
+
+    mkRHS : String -> List Binder -> Raw -> Raw
+    mkRHS instName (MkBind fc nm Explicit ty :: bs) tm = mkRHS instName bs (RApp fc tm (RVar fc "\{instName},\{nm}") Explicit)
+    mkRHS instName (b :: bs) tm = mkRHS instName bs tm
+    mkRHS instName [] tm = tm
+
+    apply : Val -> List Val -> M Val
+    apply x [] = pure x
+    apply (VPi fc nm icit a b) (x :: xs) = apply !(b $$ x) xs
+    apply x (y :: xs) = error instfc "expected pi type \{show x}"
+
 processDecl (Data fc nm ty cons) = do
   putStrLn "-----"
   putStrLn "Data \{nm}"

src/Lib/Syntax.idr

@@ -121,6 +121,7 @@ data Decl
   | PFunc FC Name Raw String
   | PMixFix FC (List Name) Nat Fixity
   | Class FC Name Telescope (List Decl)
+  | Instance FC Raw (List Decl)
 
 
 public export
@@ -154,6 +155,7 @@ Show Clause where
 Show Import where
   show (MkImport _ str) = foo ["MkImport", show str]
 
+-- this is for debugging, use pretty when possible
 covering
 Show Decl where
   show (TypeSig _ str x) = foo ["TypeSig", show str, show x]
@@ -163,7 +165,8 @@ Show Decl where
   show (PType _ name ty) = foo ["PType", name, show ty]
   show (PFunc _ nm ty src) = foo ["PFunc", nm, show ty, show src]
   show (PMixFix _ nms prec fix) = foo ["PMixFix", show nms, show prec, show fix]
-  show (Class _ nm _ _) = foo ["Class", "FIXME"]
+  show (Class _ nm tele decls) = foo ["Class",  nm, "...", show $ map show decls]
+  show (Instance _ nm decls) = foo ["Instance",  show nm, show $ map show decls]
 
 export covering
 Show Module where
@@ -261,7 +264,8 @@ Pretty Decl where
   pretty (PType _ nm ty) = text "ptype" <+> text nm <+> (maybe empty (\ty => ":" <+> pretty ty) ty)
   pretty (PFunc _ nm ty src) = "pfunc" <+> text nm <+> ":" <+> nest 2 (pretty ty <+> ":=" <+/> text (show src))
   pretty (PMixFix _ names prec fix) = text (show fix) <+> text (show prec) <+> spread (map text names)
-  pretty (Class _ _ _ _) = text "TODO pretty PClass"
+  pretty (Class _ _ _ _) = text "TODO pretty Class"
+  pretty (Instance _ _ _) = text "TODO pretty Instance"
 
 export
 Pretty Module where