Skip to content

Instantly share code, notes, and snippets.

Avatar

Víctor López Juan vlopezj

View GitHub Profile
View ProjectHeterogeneous.md

This is an explanation of the changes introduced in pull request https://github.com/agda/agda/pull/5234/

Twin context infrastructure

When checking whether two well-typed terms t and u are convertible, they might not be typed in the same context.

From the example above, we have a constraint

View Foo.hs
data EitherDup a = MyLeft a
| MyRight a
class HasEndo t where
-- | prop> endo . endo == id
endo :: t -> t
instance HasEndo (EitherDup a) where
endo (MyLeft a) = MyRight a
endo (MyRight a) = MyLeft a
View NewtypeDeriving.markdown

Monad gives Applicative, Applicative etc. gives Num, Floating, Fractional

Setting it up

WrapMonad tells us that a Monad implies Functor, Applicative

instance Monad m => Functor     (WrappedMonad m)
instance Monad m => Applicative (WrappedMonad m)
instance Monad m => Monad       (WrappedMonad m)
View FunImplicits.lagda.rst
module FunImplicits where

open import Data.Bool

data Nat : Set where
  zero : Nat