YBogomolov

import { Functor } from 'fp-ts/lib/Functor';
import { HKT, Kind3, URIS3 } from 'fp-ts/lib/HKT';

export type Fn<A, B> = (a: A) => B;

export interface Profunctor<F extends URIS3, G> {
  dimap: <A, B>(ab: Fn<A, B>) => <C, D>(cd: Fn<C, D>) => (fbc: Kind3<F, G, B, C>) => Kind3<F, G, A, D>;
}

export type UpStar<F, A, B> = (a: A) => HKT<F, B>;

YBogomolov

// Inspired by https://github.com/Munksgaard/session-types

interface Chan<Env, Protocol> {
  env_and_protocol: [Env, Protocol];
}

class Eps implements HasDual {
  readonly tag: 'Eps' = 'Eps';
  readonly dual!: Eps;
}

YBogomolov

export type Either<E, A> = [E, null] | [null, A];

type Fn<A, B> = (a: A) => B;

export const left = <E, A>(e: E): Either<E, A> => [e, null];
export const right = <E, A>(a: A): Either<E, A> => [null, a];

export const isLeft = <E, A>(e: Either<E, A>): e is [E, null] => e[1] === null;
export const isRight = <E, A>(e: Either<E, A>): e is [null, A] => e[0] === null;

YBogomolov

module AppendInjective

import Data.List.Views

%access export
%default total

appendInjectiveRight : (a, b, c : List x) -> a ++ b = a ++ c -> b = c
appendInjectiveRight [] _ _ prf = prf
appendInjectiveRight (_ :: xs) b c prf = appendInjectiveRight xs b c (cong { f = drop 1 } prf)

YBogomolov

How to use Idris 2 in devcontainer

Step 1: build executable and libraries

Use the Dockerfile below to build the Idris 2 executable and standard library:

docker build --tag=idris2 .

YBogomolov

import { Do } from 'fp-ts-contrib/lib/Do';
import { array } from 'fp-ts/lib/Array';
import { constUndefined, identity, Lazy } from 'fp-ts/lib/function';
import { Kind, URIS } from 'fp-ts/lib/HKT';
import * as Id from 'fp-ts/lib/Identity';
import { Monad1 } from 'fp-ts/lib/Monad';
import { none, Option } from 'fp-ts/lib/Option';
import { Traversable1 } from 'fp-ts/lib/Traversable';

declare module 'fp-ts/lib/HKT' {

YBogomolov

Примеры кода для статьи на Хабре о функциональной замене промисам

Статья: https://habr.com/ru/post/548622

YBogomolov

import { either } from 'fp-ts';
import { pipe } from 'fp-ts/function';
import Either = either.Either;

declare global {
  interface ErrorConstructor<T extends string = string> extends Error<T> {}

  interface Error<T extends string = string> {
    readonly tag: T;
    new<T extends string>(message?: string): Error<T>;

YBogomolov

type VersionChar =
    | '1' | '2' | '3' | '4' | '5';

type Char =
    | '0' | '1' | '2' | '3'
    | '4' | '5' | '6' | '7'
    | '8' | '9' | 'a' | 'b'
    | 'c' | 'd' | 'e' | 'f';

type Prev<X extends number> =

YBogomolov

type Split<S extends string, D extends string> = S extends `${infer T}${D}${infer U}` ? [T, ...Split<U, D>] : [S];

type Join<T extends string[], D extends string> = T extends []
  ? ''
  : T extends [infer F extends string, ...infer R extends string[]]
  ? `${F}${D}${Join<R, D>}`
  : never;

type Inflate<T> = Compact<UnionToIntersection<{ [K in keyof T]: InflateInner<T[K], K & string>; }[keyof T]>>;