msakai

CPL チュートリアル

はじめに

CPL (Categorical Programming Language) は、圏論の概念に基づいて設計されたプログラミング言語です。CPLでは、通常のプログラミング言語で「データ型」や「関数」と呼ばれるものが、圏論における「対象」と「射」として扱われます。

集合論	関数型プログラミング	CPL
集合	データ型	対象
写像	関数	射

msakai

sig E {
  join, meet : E -> one E
}
one sig top, bot in E {}

fact {
  all x, y, z : E {
    -- commutativity
    x.join[y] = y.join[x]
    x.meet[y] = y.meet[x]

msakai

{-
体 F が x + y = 1 かつ x y = 1 を満たすような元を持たない時、F ∪ {∞} は

∞ ⊛ y = y
x ⊛ ∞ = x
x ⊛ y = (x y - 1) / (x + y - 1)  if x + y ≠ 1
x ⊛ y = ∞                        otherwise

で定義される演算によって群となる。

msakai

module Bug where

import Control.Monad.Primitive
import qualified Data.HashTable.ST.Basic as H

data Symbol a = Symbol

data Node s a = Node

data Rule s a = Rule (Node s a)

msakai

module CohensKappa where

import Data.Hashable
import qualified Data.HashMap.Strict as HashMap

-- | Cohen's kappa coefficient (κ)
--
-- https://en.wikipedia.org/wiki/Cohen%27s_kappa
cohensKappa :: (Hashable c, Fractional a) => [(c,c)] -> a
cohensKappa xs = (po - pe) / (1 - pe)

msakai

from typing import Literal, Optional, Tuple, overload

@overload
def f(with_extra_info: Literal[False]) -> Tuple[int, int]: ...

@overload
def f(with_extra_info: Literal[True]) -> Tuple[int, int, str]: ...

# This overload is necessafy for type checking the last `f(with_extra_info)`.
@overload

msakai

{-# OPTIONS_GHC -Wall #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RecordWildCards #-}
-- https://en.wikipedia.org/wiki/Okapi_BM25
module OkapiBM25
  ( Database
  , mkDatabase
  , query
  ) where

msakai

import psycopg2


dsn = "postgresql://user:password@localhost:5432/"
db_name = "test_db"

conn = psycopg2.connect(dsn)
try:
    conn.set_isolation_level(psycopg2.extensions.ISOLATION_LEVEL_AUTOCOMMIT)
    with conn.cursor() as cur:

msakai

import Control.Monad
import Turtle

main :: IO ()
main = sh $
  forM_ [(1::Int)..2] $ \i -> do
    j <- select [(1::Int)..3]
    liftIO $ print (i, j)

{-

msakai

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
module QueryInterface where

-- Maybe (GHC.Exts.DictBox a)
data QueryIntefaceResult a where