Sintrastes

interface Logging {
    fun log(message: String)
}

interface Prompt {
    fun promptUser(): String
}

fun <Ctx> Ctx.exampleFn() where Ctx: Logging, Ctx: Prompt {

Sintrastes

{-# LANGUAGE ExistentialQuantification #-}

data Store a b = Store a (a -> b)

instance Functor (Store a) where
  fmap f (Store x g) = Store x (f . g) 

data Day f g a = forall b c. Day (f b) (g c) (b -> c -> a)

Sintrastes

data Expr =
    Elevation
  | Slope
  | Landcover
  | Add Expr Expr
  | Mul Expr Expr
  | Pow Expr Expr
  | Const Float
     deriving(Eq)
  

Sintrastes

interface Form<Ctx,A> {
	fun getValue(): A
}

// Note: I can do something like this, but I can't do
// something like: 
//  Form<Void, WDouble<Length, in Unit<Length> && ConvertibleTo<Meters>
val test: Form<Void, WDouble<Length, in Unit<Length>>>
	get() = TODO()

Sintrastes

/** 
 * Interface for a type that implements a
 * typesafe builder for some other type A.
 */
interface Builder<A> {
    fun build(): A?
}

/** 

Sintrastes

{-# LANGUAGE
   ConstraintKinds, 
   KindSignatures, 
   ExistentialQuantification,
   DataKinds,
   TypeFamilies,
   TypeOperators,
   AllowAmbiguousTypes,
   TypeSynonymInstances,
   FlexibleInstances,

Sintrastes

-- Example of a simple VDOM implemented using a cofree comonad.

data Cofree f a = Cofree a (f (Cofree f a))

class Diffable a where
  data Diff a :: *
  diff  :: a -> a -> Diff a

-- Could this have another parameter for "value type"?

Sintrastes

{-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}
class KComonad m w where
  extractM   :: w a -> m a
  -- extendM    :: (w a -> m b) -> w a -> m (w b)
  duplicateM :: w a -> m (w (w a))

-- Properties:
--    Any Monad is a KMonad automatically.
--    Any KMonad over a base monad m is automatically
--    a KMonad over a monad m whenever there is a monad

Sintrastes

module Main

-- | Simple implementation of the simply typed lambda calculus
--   with products, sums, and a natural number object
--   build on Haskell Curry's BCKW combinators.
-- Note: This could be extended by supplying a set of 
-- "base morphisms", and making a type that depends on those.
infixr 7 ~>
data (~>) : Type -> Type -> Type where
  -- Introduce a constant from an Idris value.

Sintrastes

class Sub x y where
  lift : x -> y

instance Sub x x where
  lift = id
 
pure : a -> a
pure x = x 

(<*>) : (Sub a' a, Sub b b') => (a -> b) -> a' -> b'