Skip to content

Instantly share code, notes, and snippets.

oplaxity cell

Greg Pfeil sellout

oplaxity cell
Block or report user

Report or block sellout

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
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>
. @ (->)
@ (Pair a)
@ (Pair a)
@ (a, a)
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))
: {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
(./Ratio/Type ./Int/Type)
(./Ratio/field ./Int/Type ./Int/ring)
" | /nix/store/d1mk2rhfrm9ml3m3hyxdala9s0aygvcd-dhall-1.18.0/bin/dhall
{ add =
λ ( t

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
scalaOrganization := "org.typelevel",
scalaVersion := "2.12.4-bin-typelevel-4",
scalacOptions := Seq(
libraryDependencies := Seq(
"org.typelevel" %% "cats-core" % "1.3.0" % "compile, test")))
addCompilerPlugin("org.spire-math" %% "kind-projector" % "0.9.8")
View metamorphism.hs
-- | 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.
:: (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
go c x =
let fb = ψ c

Keybase proof

I hereby claim:

  • I am sellout on github.
  • I am 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:

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 }
You can’t perform that action at this time.