oliver-batchelor

untilE :: (Reflex t, MonadHold t m, MonadFix m) => (a -> Bool) -> Event t a -> m (Event t a)
untilE f e = do
  last <- headE (ffilter f e)
  switchHold e (never <$ last)

holdDynUntil :: (Reflex t, MonadHold t m, MonadFix m) => (a -> Bool) -> Dynamic t a -> m (Dynamic t a)
holdDynUntil f d = buildDynamic (sample (current d)) =<< untilE f (updated d)

oliver-batchelor

data ApplyKey b a where 
  F :: ApplyKey (a -> b)
  A :: ApplyKey a
  
  
instance Reflex t => Apply (Event t) where
  evf <.> evx = fmapMaybe fromDMap e' where 
    e' merge (DMap.fromList [F :=> evf, A :=> evx])
    fromDMap m = case (DMap.lookup F m, DMap.lookup A m) of
      (Just (Identity f), Just (Identity a)) -> Just (f a)

oliver-batchelor

data ApplyKey b a where 
  F :: ApplyKey (a -> b)
  A :: ApplyKey a
  
  
instance Reflex t => Apply (Event t) where
  evf <.> evx = fmapMaybe fromDMap e' where 
    e' merge (DMap.fromList [F :=> evf, A :=> evx])
    fromDMap m = case (DMap.lookup F m, DMap.lookup A m) of
      (Just (Identity f), Just (Identity a)) -> Just (f a)

oliver-batchelor

data ApplyKey b a where 
  F :: ApplyKey (a -> b)
  A :: ApplyKey a

oliver-batchelor

timeout :: MonadWidget t m => (Event t a, Event t a) -> NominalDiffTime -> m (Event t a)
timeout (down, up) time = do
  delayed <- delay time down

  let timedOut = flip pushAlways down $ const $ mdo
        isDown <- hold True (False <$ leftmost [up, delayed])
        return $ gate isDown delayed

  switchHold never timedOut

oliver-batchelor

module SumF where

import GHC.Generics (Generic1)

import Data.Kind (Type, Constraint)
import Data.Proxy

import Data.Functor.Classes

oliver-batchelor

import Data.Type.Index
data Sum :: [Type] -> Type where
  L :: x -> Sum (x : xs)
  R :: Sum xs -> Sum (x : xs)


inj :: (Elem xs x) => x -> Sum xs
inj = inj' elemIndex

oliver-batchelor

{-# LANGUAGE TemplateHaskell, FlexibleContexts, FlexibleInstances, GADTs, DataKinds,
                     TypeInType, KindSignatures, InstanceSigs, TypeOperators,
                     ConstraintKinds, RankNTypes, ScopedTypeVariables, TypeFamilies,
                     UndecidableInstances, MultiParamTypeClasses, TypeApplications, PartialTypeSignatures #-}

$(singletons [d|
  data UNat = Zero | Succ UNat
    deriving (Eq)

  |])

oliver-batchelor

{-# LANGUAGE TemplateHaskell, FlexibleContexts, FlexibleInstances, GADTs, DataKinds,
                     TypeInType, KindSignatures, InstanceSigs, TypeOperators,
                     ConstraintKinds, RankNTypes, ScopedTypeVariables, TypeFamilies,
                     UndecidableInstances, MultiParamTypeClasses, TypeApplications, PartialTypeSignatures #-}

--{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise -fplugin GHC.TypeLits.KnownNat.Solver #-}

-- Three attempts at implementing a 'concat' operation for arbitrary dimension tensors,
-- concat dim xs ys is valid only if tensor xs and tensor ys share the same shape
-- (except for the dimension being joined)

oliver-batchelor

{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE RankNTypes #-}