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

Keybase proof

I hereby claim:

• I am sellout on github.
• I am sellout (https://keybase.io/sellout) on keybase.
• I have a public key whose fingerprint is 6A45 7A06 CB07 E916 EC88 EC74 1193 ACD1 96ED 61F2

To claim this, I am signing this object:

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

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