sellout

$ echo "../dhall-bhat/Field/terms.dhall
        Type
        ../dhall-bhat/Category/Monoidal/Set/cartesian
        ../dhall-bhat/Function/category
        ../dhall-bhat/Tuple/functor/pair
        (./Ratio/Type ./Int/Type)
        (./Ratio/field ./Int/Type ./Int/ring)
  " | /nix/store/d1mk2rhfrm9ml3m3hyxdala9s0aygvcd-dhall-1.18.0/bin/dhall
{ add =
      λ ( t

sellout

fixed-point operators

In general, finds the “fixed point” of some endofunctor, which means some type t, such that f t ~ t. The simplest operator is often called Fix, and takes advantage of a language’s primitive recursion to provide a very straightforward definition:

newtype Fix f = Fix { unfix :: f (Fix f) }

There are some problems with this, however:

1. most languages provide general recursion (and, in fact, this definition requires it), so such a definition can’t be total; and

sellout

inThisBuild(Seq(
  scalaOrganization := "org.typelevel",
  scalaVersion := "2.12.4-bin-typelevel-4",
  scalacOptions := Seq(
    "-Ykind-polymorphism",
    "-Yno-imports"),
  libraryDependencies := Seq(
    "org.typelevel" %% "cats-core" % "1.3.0" % "compile, test")))

addCompilerPlugin("org.spire-math" %% "kind-projector" % "0.9.8")

sellout

-- === The Abstract ===

-- | A wrapper for `Applicative`-only semantics for types that also have a
--  `Monad`.
newtype Par m a = Par { unPar :: m a }

-- | A wrapper for `Monad` semantics for types that have a distinct
--  `Applicative`.
newtype Seq m a = Seq { unSeq :: m a }

sellout

module Data.Exofunctor

import Data.Morphisms

%access public export
%default total

-- replace Control.Category with this
interface Category (cat : k -> k -> Type) where
  id  : cat a a

sellout

Verifying my Blockstack ID is secured with the address 1Ec6qRCQRbNmTAc8DY5TN3o9bd15dxrVPN https://explorer.blockstack.org/address/1Ec6qRCQRbNmTAc8DY5TN3o9bd15dxrVPN

sellout

-- | A “flushing” 'stream', with an additional coalgebra for flushing the
--   remaining values after the input has been consumed. This also allows us to
--   generalize the output away from lists.
fstream
  :: (Cursive t (XNor a), Cursive u f, Corecursive u f, Traversable f)
  => Coalgebra f b -> (b -> a -> b) -> Coalgebra f b -> b -> t -> u
fstream ψ g ψ' = go
  where
    go c x = 
      let fb = ψ c

sellout

module Polys

import Control.Monad.Identity
import Data.Morphisms

data ProductMeh: (Type -> Type) -> (Type -> Type) -> Type -> Type where
  Prod: (f a, g a) -> ProductMeh f g a

data NaturalTransformation : (Type -> Type) -> (Type -> Type) -> Type where
  NT : (f a -> g a) -> NaturalTransformation f g

sellout

> darwin-rebuild switch                  ~/.nix-defexpr/darwin
building the system configuration...
error: file ‘darwin’ was not found in the Nix search path (add it using $NIX_PATH or -I), at (string):1:1
error: Changed <darwin> but target does not exist, aborting activation
Add the darwin repo as a channel or set NIX_PATH:
$ sudo nix-channel --add https://github.com/LnL7/nix-darwin/archive/master.tar.gz darwin
$ sudo nix-channel --update

or set

sellout

module Example

interface Base (f : x -> Type) where
  base : (x -> Type) -> x -> Type

interface Base f => Corecursive (f : x -> Type) where
  cbase : (x -> Type) -> x -> Type
  cbase {f} = base {f}

-- When checking right hand side of Example.default#cbase with expected type