Skip to content

Instantly share code, notes, and snippets.

Avatar
💭
Well-typed API for the world

Nickolay Platonov canonic-epicure

💭
Well-typed API for the world
View GitHub Profile
View effectful.ts
type Effect = { kind : string }
type EffectHandler<E extends Effect> = (e : E) => unknown
function runGeneratorSyncWithEffect<ResultT, YieldT extends Effect, ArgsT extends any[]> (
effectHandler : EffectHandler<YieldT>,
func : (...args : ArgsT) => Generator<YieldT, ResultT, any>,
args : ArgsT,
scope? : any
) : ResultT
{
View exp.agda
module Exprm_FunctionImage where
open import Data.Vec
open import Data.List
case_of_ : {a b} {A : Set a} {B : Set b} A (A B) B
case x of f = f x
module FunctionImage where
data FunctionImage1 : {A B : Set} -> (f : A -> B) -> A -> B -> Set where
View random.idr
data Action = Flower | Upwards | Branch
data RndGen
RndNumGen : Type
RndNumGen = EffM Identity Action [RND] (const [RND])
getRnd : RndNumGen -> (Action, RndNumGen)
getRnd prev =
let
View name.idr
module Language
import Data.So
%default total
record SomeRec where
constructor MkSomeRec
WhereCondition : Bool
View record.idr
module Language
import Data.So
%default total
-- typechecks after removing "mutual"
mutual
record SomeRec where
constructor MkSomeRec
View agda_question.agda
module SQL where
open import Data.Nat
a : Nat
a = 1
{-
View totality.idr
module SQL
%default total
%access public export
data SqlType = BOOLEAN | INTEGER
mutual
data ColumnExpression : SqlType -> Type where
BooleanLiteral : Bool -> ColumnExpression BOOLEAN
View question.idr
module Algebra
data ExprF : (carrier : Type) -> Type where
Const : Int -> ExprF carrier
Add : (a : carrier) -> (b : carrier) -> ExprF carrier
Mul : (a : carrier) -> (b : carrier) -> ExprF carrier
data Fix : (f : Type -> Type) -> Type where
In : f (Fix f) -> Fix f
View test.idr
module Language
%default total
mutual
data QuerySource : Type where
Table : (tableName : String) -> QuerySource
SubQuery : Bool -> QuerySource
As : (source : QuerySource) -> {auto prf : QuerySourceIsNotAliased source} -> (aliasName : String) -> QuerySource
View totality.idr
module Language
import Control.Monad.State
%default total
%access public export
mutual
record QueryAbstractSyntaxTree where