91 lines
3.2 KiB
Plaintext
91 lines
3.2 KiB
Plaintext
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) ->
|
|
Monad M
|
|
|
|
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
|
|
|
|
EitherMonad : {A : U} -> Monad (Either A)
|
|
EitherMonad = MkMonad {Either A} (\ ma amb =>
|
|
-- ^ Need this for scrut type to be non-meta
|
|
case ma of
|
|
Left a => Left a
|
|
Right b => amb b)
|
|
|
|
-- [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)
|
|
|
|
-- So the idea here is to have some implicits that are solved by 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
|
|
|
|
infixl 1 _>>=_
|
|
|
|
ptype Int
|
|
|
|
-- For now, we may try to solve this at creation time, but it's possible postpone is needed
|
|
|
|
-- *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.)
|
|
|
|
foo : Int -> Maybe Int
|
|
foo x = _>>=_ {_} {_} {_} {_} (Just x) (\ x => Just 10)
|
|
-- ^
|
|
/-
|
|
So, agda style we'd guess ?m8 is MonadMaybe or MonadEither - agda's "maybe" case
|
|
|
|
-/
|