ohnosequences / stuff

Useful stuff.
GNU Affero General Public License v3.0
1 stars 0 forks source link

Naked recursive types #68

Closed eparejatobes closed 6 years ago

eparejatobes commented 6 years ago
// is it worthwhile?
import sums._
import products._
import functions._
import scala.Int

type List[X] >: ∗ + (X × List[X]) <: ∗ + (X × List[X])

def head[X]: List[X] -> (∗ + X) =
  +-[∗] at left
def tail[X]: List[X] -> (∗ + List[X]) =
  +-[∗] at right

def Nil[X]: List[X] =
  inL at ∗
def cons[X]: (X × List[X]) -> List[X] =
  inR

implicit class ListOps[X](xs: List[X]) {

  def ::(x: X): List[X] = cons(x and xs)
}

val l = 1 :: 2 :: 3 :: 4 :: Nil
eparejatobes commented 6 years ago

Not worth the contortions, closing.