zraffer

{-# OPTIONS --type-in-type  #-}

module Hurkens where

-----------------------

O = Set

Bottom : O
Bottom = (A : O) → A

zraffer

package cat

object CAT {

  // system traits
  sealed trait Type[Self <: Type[Self]]
  sealed trait Of[Self <: Of[Self, T], T <: Type[T]]

  // types
  case class Ob()

zraffer

// Scala Types are objects of Cartesian Closed Category
// (w/o equalities, probably not a category, sorry)
object CCC {

  // category structure
  def id[T0]: T0=>T0 = x0=>x0
  def mul[T1, T2, T3](f23: T2=>T3, f12: T1=>T2): (T1=>T3) = x1 => f23(f12(x1))

  // terminal object; adjunction;
  type _1_ = Unit

zraffer

sealed trait Free[F[_], A] { self =>
  final def map[B](ab: A => B): Free[F, B] = Free.flatMap(self, ab andThen (Free.point[F, B](_)))
  final def flatMap[B](afb: A => Free[F, B]): Free[F, B] = Free.flatMap(self, afb)
  final def interpret[G[_]: Monad](fg: F ~> G): G[A] = self match {
    case Free.Point(a0) => a0().point[G]
    case Free.Effect(fa) => fg(fa)
    case fm : Free.FlatMap[F, A] =>
    	val ga0 = fm.fa.interpret[G](fg)
    	ga0.flatMap(a0 => fm.afb(a0).interpret[G](fg))
  }

zraffer

ok
<<"( λ (P.el: ( ∀ (_: ( ∀ (A.Carrier.El: *1)\n    → ( ∀ (A.Carrier.To: ( ∀ (a: A.Carrier.El)\n      → ( ∀ (b: A.Carrier.El)\n      → *0)))\n    → ( ∀ (A.Carrier.Trans: ( ∀ (e1: A.Carrier.El)\n      → ( ∀ (e2: A.Carrier.El)\n      → ( ∀ (e3: A.Carrier.El)\n      → ( ∀ (_: ((A.Carrier.To e1) e2))\n      → ( ∀ (_: ((A.Carrier.To e2) e3))\n      → ((A.Carrier.To e1) e3)))))))\n    → ( ∀ (A.Mk.el: A.Carrier.El)\n    → ( ∀ (A.Mk.ok: ((A.Carrier.To A.Mk.el) A.Mk.el))\n    → A.Carrier.El))))))\n  → *0))\n→ ( λ (P.ok: ( ∀ (a1.el: ( ∀ (A.Carrier.El: *1)\n    → ( ∀ (A.Carrier.To: ( ∀ (a: A.Carrier.El)\n      → ( ∀ (b: A.Carrier.El)\n      → *0)))\n    → ( ∀ (A.Carrier.Trans: ( ∀ (e1: A.Carrier.El)\n      → ( ∀ (e2: A.Carrier.El)\n      → ( ∀ (e3: A.Carrier.El)\n      → ( ∀ (_: ((A.Carrier.To e1) e2))\n      → ( ∀ (_: ((A.Carrier.To e2) e3))\n      → ((A.Carrier.To e1) e3)))))))\n    → ( ∀ (A.Mk.el: A.Carrier.El)\n    → ( ∀ (A.Mk.ok: ((A.Carrier.To A.Mk.el) A.Mk.el))\n    → A.Carrier.El))))))\n  → ( ∀ (a1.ok: ( ∀ (A1.

zraffer

namespace foo

	definition bool := ∀ a : Prop, a → a → a
	definition tt : bool := λ (a : Prop) (c d : a), c
	definition ff : bool := λ (a : Prop) (c d : a), d

	definition ind_on_T := ∀ P : bool → Prop, ∀ a : bool, P tt → P ff → P a
	definition ind_on : ind_on_T := λ (P : bool → Prop) (a : bool) (t : P tt) (f : P ff), a (P a) t f
	check ind_on

zraffer

-- #Prop
*

zraffer

Fix : (Type -> Type) -> Type
Fix f = {x : Type} -> (f x -> x) -> x

fold : Functor f => {x : Type} -> (f x -> x) -> Fix f -> x
fold k t = t k

embed : Functor f => f (Fix f) -> Fix f
embed s k = k (map (fold k) s)

project : Functor f => Fix f -> f (Fix f)

zraffer

%default total

data Mu : (Type -> Type) -> Type where
    In : f (Mu f) -> Mu f

out : Mu f -> f (Mu f)
out (In x) = x

data LstF : Type -> Type -> Type where
    LF : ({c : Type} -> (Maybe (a, Unit -> c, b) -> c) -> c) -> LstF a b

zraffer

{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE Rank2Types #-}

import Data.Maybe

data List a = L (forall b. (Maybe (a, (b, List a)) -> b) -> b)

nil :: List a
nil = L (\f -> f Nothing)