Odomontois

import java.io.{BufferedReader, BufferedWriter, FileReader, FileWriter}
import java.nio.file.Paths
import java.util.concurrent.TimeUnit

import cats.effect.{Clock, ExitCode, Resource}
import cats.implicits._
import monix.eval.{Task, TaskApp}
import monix.execution.atomic.Atomic
import monix.execution.{Ack, Cancelable, Scheduler}
import monix.nio.file

Odomontois

object TagTest {
  def fooManual(coco: Coco): Coco = coco
  def fooSuperTagged(coco: Coca): Coca = coco

  object Coco extends TaggedInt
  type Coco = Coco.T

  object Coca extends TaggedType[Int]
  type Coca = Coca.Type
}

Odomontois

Compiled from "FooOps.scala"
public final class maccc.Foo$ {
  public static final maccc.Foo$ MODULE$;

  public static {};
    Code:
       0: new           #2                  // class maccc/Foo$
       3: dup
       4: invokespecial #17                 // Method "<init>":()V
       7: putstatic     #19                 // Field MODULE$:Lmaccc/Foo$;

Odomontois

{-# LANGUAGE AllowAmbiguousTypes       #-}
{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE DeriveAnyClass            #-}
{-# LANGUAGE DeriveGeneric             #-}
{-# LANGUAGE DuplicateRecordFields     #-}
{-# LANGUAGE FlexibleContexts          #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE TypeApplications          #-}

import           Control.Lens

Odomontois

  val parseDateTime: Parsing[String, LocalDateTime] = parsing { (s: V[String]) =>
    val (dayStr, rest1)        = sep(".")(s)
    val (monthStr, rest2)      = sep(".")(rest1)
    val (yearStr, rest3)       = sep(" ")(rest2)
    val (hourStr, rest4)       = sep(":")(rest3)
    val (minuteStr, secondStr) = sep(":")(rest4)
    ----
    val year   = readInt(yearStr)
    val month  = readInt(monthStr)
    val day    = readInt(dayStr)

Odomontois

def retrieve[Entity] : Id[Entity] -> (Entity x Database) = ???
def currentOrder: User -> (OrderId, User) = ???
def update[Entity](field: Field[Entity])(value: field.Type) : Entity -> (Entity  x Invalid)= ???
def save[Entity] : Entity -> (Database x Invalid) = ???

def finishCurrentOrder: UserId -> (Invalid x Database) = db { userId =>   
  var error: Invalid = empty
  var database: Database = empty
  var user : User = later
  var order: Order = later  

Odomontois

import cats.{Eval, Monad}
import cats.data.Kleisli
import volga.syntax.comp._
import volga.syntax.arr._
import volga.syntax.cat._
import cats.syntax.applicative._
import cats.syntax.flatMap._
import cats.syntax.functor._

import scala.io.StdIn

Odomontois

  trait Num[N] {
    def plus(x: N, y: N): N
    def mul(x: N, y: N): N
    def fromInt(x: Int): N

    def one: N            = fromInt(1)
    def zero: N           = fromInt(0)
    def negate(x: N): N   = mul(x, fromInt(-1))
    def minus(x: N, y: N) = plus(x, negate(y))
  }

Odomontois

type Not[b <: Boolean] <: Boolean = b match {
    case false => true
    case true => false
}

sealed trait Lst[+A]{
    type IsEmpty <: Boolean    
    def isEmpty: IsEmpty
    def notEmpty : Not[IsEmpty] 
}

Odomontois

\import Data.Bool
\import Equiv (QEquiv)
\import Equiv.Univalence
\import Paths

\lemma not-involutive (b : Bool) : not (not b) = b
  | true => idp
  | false => idp

\func boolInv : Bool = Bool => QEquiv-to-= (\new QEquiv not not not-involutive not-involutive)