Skip to content

Instantly share code, notes, and snippets.

Avatar
⛓️
oplaxity cell

Greg Pfeil sellout

⛓️
oplaxity cell
View GitHub Profile
View categorize-abst.hs
-- step>
(abst @ (Pair a) ($fHasRepPair @ a))
`cast` (Sub (D:R:RepPair[0] <a>_N) ->_R <Pair a>_R
:: Coercible (Rep (Pair a) -> Pair a) ((a, a) -> Pair a))
-- result>
. @ (->)
$fCategory->
@ (Pair a)
@ (Pair a)
@ (a, a)
@sellout
sellout / OpClasses.idr
Last active Aug 21, 2019
Defining ad-hoc polymorphism using dependently-typed implicits.
View OpClasses.idr
-- This illustrates (most of) a new(?) encoding of ad-hoc polymorphism using
-- dependent types and implicits.
--
-- Benefits of this approach:
-- • can have multiple “ambiguous” instances without requiring things like
-- Haskell’s newtypes to distinguish them;
-- • can disambiguate instances with minimal information, rather than having to
-- know some arbitrary instance name as you would with a system like Scala’s
-- implicits;
-- • implementers don’t need to know/provide the full family of instances – they
View OpClassesRepro.idr
module OpClassesRepro
record SemigroupRec (t : Type) (op : t -> t -> t) where
constructor SemigroupInfo
associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))
resolveSemigroup
: {auto associative : (a : t) -> (b : t) -> (c : t) -> (op (op a b) c = op a (op b c))}
-> SemigroupRec t op
resolveSemigroup {associative} = SemigroupInfo associative
View gist:f5e36cd4625f9922456a8cad945eaa09
$ 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
View fixed-point-operators.md

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
View build.sbt
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")
View par-seq.hs
-- === 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 }
View Exofunctor.idr
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
View gist:58c2ce8b3ef8f23789ac9d41dfeba46b
Verifying my Blockstack ID is secured with the address 1Ec6qRCQRbNmTAc8DY5TN3o9bd15dxrVPN https://explorer.blockstack.org/address/1Ec6qRCQRbNmTAc8DY5TN3o9bd15dxrVPN
You can’t perform that action at this time.