googleson78

data A = A ()
  deriving Show

a :: A
a = (f a)

f :: A -> A
f (A x) = A ()

googleson78

-- empty type
data ⊥ : Set where

-- can't prove this so we introduce it as an axiom
postulate
    stab : ∀{A : Set} -> ((A -> ⊥) -> ⊥) -> A

-- if you give me an x of type X and an inhabitant of P x, then I have proof that there exists an inhabitant of P x
data ∃ {X : Set} (P : X -> Set) : Set where
    intro-∃ : ∀(x : X) -> P x -> ∃ P

googleson78

    Fusion
      fusion
        Union proofs should simplify FAILED [1]
        internal uses of StateT should simplify
        internal uses of ExceptT should simplify
        `runState . reinterpret` should fuse
        who needs Sematic even?
    Output
      runBatchOutput
        should return nothing at batch size 0

googleson78

tauren :: /tmp/liquid » tree
.
├── Crash.hs
└── include
    └── Data
        └── Text.spec

2 directories, 2 files

tauren :: /tmp/liquid » cat Crash.hs

googleson78

{-# LANGUAGE GADTs #-}

instance Бурито Списък where
  (✨) хикс = хикс `СлепенС` ПразенСписък
  списъкОтМесо 🔜 рецептаЗаБуритоСМесоИЗеленчуци =
    (💥) ((📄) рецептаЗаБуритоСМесоИЗеленчуци списъкОтМесо)

class Бурито обвивка where
  (✨) :: месо -> обвивка месо
  (🔜) :: обвивка месо -> (месо -> обвивка месоСъсЗеленчуци) -> обвивка месоСъсЗеленчуци

googleson78

-- boilerplate - име на модула
module Even where

-- `X : Y`
-- означава "X е от тип Y"

-- типова декларация
-- казва че "има нещо което се казва One"
-- и то е тип (": Set" частта това означава, нека мислим че Set е същото като Тип)

googleson78

{-# LANGUAGE DerivingVia #-}
{-# LANGUAGE DerivingStrategies #-}

module HashAbuse where

import Data.Hashable
import Data.Function (on)

newtype Vertical = Vertical {getVertical :: (Int, Int)}
  deriving stock Show

googleson78

module Product where

data Nat : Set where
  zero : Nat
  suc : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

_+_ : Nat -> Nat -> Nat
zero + m = m

googleson78

{-# LANGUAGE TypeOperators #-}

data (:+:) a b
  = Inl a
  | Inr b

data (:*:) a b
  = a :*: b

data One = One

googleson78

data Lambda
  = Var Name
  | App Lambda Lambda
  | Lam Name Lambda
  deriving (Eq, Show)

name :: Parser Name
name = lexeme $ sat \x -> if x `elem` "xyzuvw" then Just $ Name [x] else Nothing

var :: Parser Lambda