MarcelineVQ

using (p : a -> Type)

  -- codata Stream a = (::) a (Stream a)

  data Eventually_s : Stream a -> Type where
    Ev_b : p x -> Eventually_s (x :: xs)
    Ev_r : p x -> Eventually_s xs -> Eventually_s (x :: xs)

  eventually_s_inv : Eventually_s s -> s = x :: s' -> p x -> Eventually_s s'
  eventually_s_inv r@(Ev_b y) prf px = ?what

MarcelineVQ

data LQueue : Nat -> Type -> Type where
  MkQ : (xs : Vect ln a)
     -> (ys : Vect rn a)
     -> LQueue (ln + rn) a

-- an invariant checker
queue : LQueue n a -> LQueue n a
queue (MkQ xs {ln} ys {rn}) with (isLTE rn ln)
  queue (MkQ xs ys) | (Yes prf) = MkQ xs ys

MarcelineVQ

-- available methods
record Method where
  constructor MkMethod
  name : String
  args : Type
  {prf : So (not $ "rpc." `isPrefixOf` name)}
  
-- I'd like to be able to write
gorb : Method
gorb = MkMethod "foo" ()

MarcelineVQ

interface Foo a where
  Gob : Type
  plu : a -> Gob -> Gob

implementation
Foo Char where
   Gob = List Char
   plu = (::)

MarcelineVQ

import Control.Applicative

data Coroutine s m r = MkCo { resume :: m (Either (s (Coroutine s m r)) r)}

instance (Functor s, Functor m) => Functor (Coroutine s m) where
  fmap f x = MkCo $ fmap (either (Left . fmap (fmap f)) (Right . f)) (resume x)

instance (Functor s, Applicative m) =>
  Applicative (Coroutine s m) where
    pure = MkCo . pure . Right

MarcelineVQ

data Trampoline : (m : Type -> Type) -> (r : Type) -> Type where
  MkTram : m (Either (Trampoline m r) r) -> Trampoline m r

partial
Functor m => Functor (Trampoline m) where
  map f (MkTram x) = MkTram (map (either (Left . map f) (Right . f)) x)

   |
40 |   map f (MkTram x) = MkTram (map (either (Left . map f) (Right . f)) x)
   |   ~~~~~~~~~~~~~~~~~

MarcelineVQ

mutual
  data Trampoline : (m : Type -> Type) -> (r : Type) -> Type where
    MkTram : m (TrampOneOR m r) -> Trampoline m r

  data TrampOneOR : (m : Type -> Type) -> (r : Type) -> Type where
    Loft : Trampoline m r -> TrampOneOR m r
    Roght : r -> TrampOneOR m r

MarcelineVQ

-- m can be a Monad
data Trampoline : (m : Type -> Type) -> (r : Type) -> Type where
  MkTram : m (Either (Trampoline m r) r) -> Trampoline m r

MarcelineVQ

-- fix 1

instance Monoid a => Semigroup (Optional a) where
      (<>) = mappend
instance Monoid a => Monoid (Optional a) where
      mempty = Nada
      mappend Nada Nada = Nada
      mappend (Only x) Nada = Only x
      mappend Nada (Only x) = Only x
      mappend (Only x) (Only y) = Only (x <> y)

MarcelineVQ

<jellostahps> so doubling every char of a String is grow :: String -> String
<jellostahps> grow(x:xs) = x:x:grow(xs)
<jellostahps> what about every index of a character is repeated that many times
<jellostahps> input=string output = s t t r r r i i i i n n n n n g g g g g g
<pikajude> grow "string" = "sttrrriiiinnnnngggggg"
<pikajude> may not work for all inputs
<jellostahps> yeah, wondering what i can do to fix it
<jellostahps> would it definitely require a second function
<dmwit> > concat (zipWith replicate [1..] "string")
<lambdabot>  "sttrrriiiinnnnngggggg"