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