googleson78

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

googleson78

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

data Foo = Foo

googleson78

{-# LANGUAGE TypeFamilies #-}
module Ado where

(>>=) :: Int ~ Char => f a -> (a -> f b) -> f b
(>>=) = undefined

(<*>) :: Applicative f => f (a -> b) -> f a -> f b
(<*>) = (Prelude.<*>)

pure :: Applicative f => a -> f a

googleson78

Подготовка за работа с Agda

0. Инсталирате си Emacs (по възможност използвайки package manager-а ви)

   Не съм сигурен как става под windows, но има инструкции на GNU сайта, както и в spacemacs github-a например. Или пък това?

За инсталиране на самата Agda има вариант или да се компилира, или да се използва пакет от системата.

Например за arch linux хората в AUR има обновен пакет, но тъй като много дистрибуции, например debian/ubuntu (особено stable вариантите им)

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

googleson78

{-# LANGUAGE TypeOperators #-}

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

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

data One = One

googleson78

module Product where

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

{-# BUILTIN NATURAL Nat #-}

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

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

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

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

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

googleson78

{-# LANGUAGE GADTs #-}

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

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