Emacs mód pro Agdu napíše kód za vás

17.2.2013 19:45 | Přečteno: 1169× | Programování | | poslední úprava: 17.2.2013 19:45

V tomto zápisku si ukážeme jednu užitečnou schopnost Emacs módu pro jazyk Agda. Jedná se o automatické napsání kódu, kdy programátor pouze specifikuje, co má kód dělat, a nechá editor, aby takový kód napsal.

Naším cílem bude napsat funkci zap. zap dostane seznam funkcí a stejně dlouhý seznam prvků a na každý prvek aplikuje odpovídající funkci. Například výsledkem zap (suc ∷ suc ∷ id ∷ (suc ∘ suc) ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) bude seznam 2 ∷ 3 ∷ 3 ∷ 6 ∷ []. Pro pořádek doplňme, že suc x je číslo o jedna větší než x (od slova successor), id je identita, ∘ značí skládání funkcí, ∷ značí cons (dostane prvek a seznam a zkonstruuje nový seznam, který začíná daným prvkem a pokračuje daným seznamem) a [] značí prázdný seznam (například 0 ∷ [] je seznam obsahující číslo 0).

Jazyk Agda je minimalistický – čísla ani seznamy nejsou jeho součástí, tudíž aby fungoval příklad uvedený výše, budeme muset napsat funkce id, ∘ a zap a definovat datový typ pro přirozená čísla ℕ a datové typy pro seznamy Vec.

Začneme identitou – funkcí, která vrátí to, co dostane. Napíšeme typ, levou stranu funkce a místo pravé strany dáme otazník (kód, který patří místo otazníku, bude doplněn automaticky):

id : {A : Set} → A → A
id x = ?

Funkce má dva parametry – množinu a její prvek. Složené závorky kolem prvního parametru značí, že se jedná o implicitní parametr – kompilátor se pokusí doplnit argument automaticky. Nyní Emacs požádáme, aby doplnil kód. Nejprve použijeme příkaz Load (C-c C-l), ten provede zvýraznění kódu a otazník změní na chlívek { }0 vymezený složenými závorkami (mezi složené závorky jde psát). Chlívek můžeme chápat jako díru ve zdrojovém kódu, kterou je třeba vyplnit. Chlívky jsou očíslovány (náš má číslo 0) a lze se mezi nimi pohybovat pomocí příkazů Next Goal (C-c C-f) a Previous Goal (C-c C-b). Když je kurzor v chlívku, lze použít příkaz Auto (C-c C-a) a Emacs se pokusí napsat kód automaticky. V tomto případě Emacs automaticky napíše x:

id : {A : Set} → A → A
id x = x

Tento příklad pravděpodobně člověka na zadek neposadí, zkusme skládání funkcí. Postup je stejný. Napíšeme typ, levou stranu funkce a místo pravé strany dáme otazník:

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘ f = ?

Podtržítka v názvu funkce _∘_ značí místa, kam přijdou argumenty (například if—then—else lze definovat jako funkci if_then_else_ se třemi parametry). ∘ pro skládání funkcí má tři implicitní parametry. Nyní požádáme Emacs o doplnění kódu (příkaz Load, přesun do vzniklého chlívku, příkaz Auto) a dostaneme:

_∘_ : {A B C : Set} → (B → C) → (A → B) → (A → C)
g ∘ f = λ z → g (f z)

Emacs doplnil λ z → g (f z). Tohle už je zajímavajší, ne?

Vec budou seznamy opatřené délkou (součástí typu bude i délka seznamu). Délku budeme reprezentovat přirozeným číslem. Napřed tedy nadefinujeme množinu přirozených čísel:

data ℕ : Set where
  zero : ℕ
  suc  : ℕ → ℕ

Význam definice:

• První řádek definice říká: „ℕ je nejmenší množina pro níž platí“.
• Druhý řádek říká: „množina ℕ obsahuje zero“ (rozuměj: nula je přirozené číslo).
• Třetí řádek říká: „obsahuje-li množina ℕ prvek n, pak také obsahuje prvek suc n“ (rozuměj: je-li n přirozené číslo, pak i n + 1 je přirozené číslo).

Přirozená čísla 0, 1, 2, 3 pak zapisujeme zero, suc zero, suc (suc zero), suc (suc (suc zero)) Abychom mohli používat známý zápis v desítkové soustavě, řekneme Agdě následující:

{-# BUILTIN NATURAL ℕ    #-}
{-# BUILTIN ZERO    zero #-}
{-# BUILTIN SUC     suc  #-}

Zápisem 2 pak Agda bude rozumět suc (suc zero). Nyní můžeme zadefinovat seznamy s délkou (seznamy bez délky se často označují jako List a ty s délkou jako Vec nebo Vector). Na rozdíl od přirozených čísel nedefinujeme jednu množinu, ale celou rodinu množin. Pro každou množinu A a přirozené číslo n definujeme množinu seznamů délky n s prvky z množiny A:

data Vec (A : Set) : ℕ → Set where
  []  : Vec A zero
  _∷_ : {n : ℕ} → A → Vec A n → Vec A (suc n)

Význam definice:

• První řádek říká: „pro množinu A a přirozené číslo n je Vec A n nejmenší množina pro níž platí“.
• Druhý řádek říká: „[] je v množině Vec A zero“ (rozuměj: prázdný seznam patří do množiny seznamů délky nula).
• Třetí řádek říká: „je-li x prvek z množiny A a xs je seznam délky n nad množinou A, tak x ∷ xs je seznam délky n + 1 nad množinou A“.

Aby se ∷ parsoval jako doprava asociativní, je třeba přidat následující řádek:

infixr 5 _∷_

Konečně můžeme definovat funkci zap. Budeme postupovat stejně jako v předchozích případech. Napíšeme typ funkce, levou stranu a místo pravé strany dáme otazník:

zap : {A B : Set} {n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
zap fs xs = ?

Příkazem Load vytvoříme chlívek. Když bychom nyní zajeli kurzorem do chlívku a použili příkaz Auto, doplnění kódu se nepodaří. Funkci je třeba definovat rozborem případů a to standardně Auto nedělá. Do chlívku je třeba napsat -c, což povolí rozbor případů (case split) a nyní můžeme použít příkaz Auto a Emacs napíše

zap : {A B : Set} {n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
zap [] xs = []
zap (x ∷ x₁) (x₂ ∷ x₃) = x x₂ ∷ zap x₁ x₃

Kód je v pořádku až na pojmenování proměnných, to už musíme opravit ručně:

zap : {A B : Set} {n : ℕ} → Vec (A → B) n → Vec A n → Vec B n
zap [] _ = []
zap (f ∷ fs) (x ∷ xs) = f x ∷ zap fs xs

Všimněte si, že v definici funkce chybí případ, kdy je seznam funkcí prázdný a seznam prvků neprázdný. Důvodem je, že typ funkce zap říká, že všechny seznamy mají délku n (jsou tedy stejně dlouhé).

Drobná potíž je, že ne vždy příkaz Auto najde program, který požadujeme. Ukážeme si to na příkladu s funkcí not, která by měla negovat booleovskou hodnotu. Protože Agda neobsahuje typ Bool, musíme ho napřed zadefinovat:

data Bool : Set where
  true  : Bool
  false : Bool

Nyní můžeme chtít napsat funkci not:

not : Bool → Bool
not x = ?

Po využití příkazu Auto dostaneme:

not : Bool → Bool
not x = x

To je ale špatně, chtěli jsme:

not : Bool → Bool
not true  = false
not false = true

Další informace o příkazu Auto je možné najít na stránkách Agdy. Na závěr můžeme pomocí příkazu Evaluate term to normal form (C-c C-n) vyzkoušet, zda zap funguje. A opravdu, po stisku kláves C-c C-n a zadání zap (suc ∷ suc ∷ id ∷ (suc ∘ suc) ∷ []) (1 ∷ 2 ∷ 3 ∷ 4 ∷ []) dostaneme výsledek 2 ∷ 3 ∷ 3 ∷ 6 ∷ [].        

Komentáře

[Bystroushaak]

Hipster level: over 9000.

[petr_p]

Výborný zápisek. I když tohle typové odvozování naruby (z datového typu udělat kostru generátoru) mi zas tak zázračné nepřijde. Zápisek mě ale utvrdil, že Unicode je dobrý nápad. Škoda, že většina jazyků potupně aproximuje v ASCII.

[lm]

Hezka hracka :) Pripomnelo mi to Djinn pro Haskell. IMHO to ale moc prakticky neni. Ani v striktnejsim typovem systemu Agdy to zadny extra kouzla neumi.

Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:

-- nejprve operator ekvivalence
(==) :: Eq a => a -> a -> Bool

-- nerovnost ?
(/=) ? Eq a => a -> a -> Bool
-- error: cannot infer
-- musi natukat clovek
x /= y == not (x == y)
-- a je to :)

[lm]

eh, jedno rovnitko navic. Ta definice mela byt:

x /= y = not (x == y)

[Radek Miček]

Bez lidske inteligence si nemuze poradit ani s takovou trivialitou jako je treba odvozeni funkce (operatoru) nerovnosti:

Docela mě překvapuje, že to nevrátí třeba x /= y = True.

Příkaz Auto zvládne doplnit i složitější výrazy. Například return a bind pro stavovou monádu doplní takto:

record Pair (A B : Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B

record State (S A : Set) : Set where
  constructor state
  field
    runState : S → Pair S A

-- vygenerovane prikazem Auto
return : {S A : Set} → A → State S A
return x = state (λ z → z , x)

-- vygenerovane prikazem Auto (a spatne)
bind : {S A B : Set} → State S A → (A → State S B) → State S B
bind m f = state
             (λ z →
                z ,
                Pair.proj₂
                (State.runState (f (Pair.proj₂ (State.runState m z))) z))

bind je bohužel špatně – typ totiž nezakazuje použití původního stavu. Když ale umožním, aby se typ stavu měnil (pak už to není monáda), tak Auto vygeneruje již korektní definici i pro bind:

record IState (S₁ S₂ A : Set) : Set where
  constructor state
  field
    runState : S₁ → Pair S₂ A

-- vygenerovane prikazem Auto
ibind : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind m f = state
              (λ z →
                 Pair.proj₁
                 (IState.runState (f (Pair.proj₂ (IState.runState m z)))
                  (Pair.proj₁ (IState.runState m z)))
                 ,
                 Pair.proj₂
                 (IState.runState (f (Pair.proj₂ (IState.runState m z)))
                  (Pair.proj₁ (IState.runState m z))))

Nicméně perfektní to není – některé výrazy se tam zbytečně opakují, člověk by napsal:

-- napsane clovekem
ibind' : {S₁ S₂ S₃ A B : Set} → IState S₁ S₂ A → (A → IState S₂ S₃ B) → IState S₁ S₃ B
ibind' m f = state
              (λ st₁ →
                 let (st₂ , a) = IState.runState m st₁
                 in IState.runState (f a) st₂)

IMHO to ale moc prakticky neni.

Hodí se to v důkazech. Tam potřebuji najít term s daným typem a už příliš nezáleží na tom, jak ten term vypadá.

[coder]

Vyzkouším až se zase odhodlám učit Emacs. Poslední pokus mi způsobil úkrutnou fóbii. Snad to někdy překonám.

[Josef Kufner]

Tak to radši zkus Vim

[coder]

Bez Vimu si jiz nedokazi predstavit svuj zivot

Ale ten Emacs ma spousty zajimavych funkci a doplnku, ktere bych rad pouzival a ve svete vimu jsou nedokonale imitovane. Napr. org mod a velmi kvalitni integrace REPLu funkcionalnich jazyku. No uvidim, treba se nekdy hacknu.

[JS]

Hm, moc tomu nerozumim, ale prijde mi to s tou Agdou asi trochu jako s mym otcem, co uz zapomina - prestoze trva na tom, ze mu mam vysvetlit, jak se veci (na pocitaci) delaji, aby mi "usetril praci", je proste daleko jednodussi, kdyz to udelam za nej..

[Radek Miček]

Hm, moc tomu nerozumim

Máte nějaký konkrétní dotaz, třeba bych mohl pomoci?

Mně se na Agdě a podobných jazycích líbí minimalističnost kombinovaná se silou typového systému. Naopak mi vadí absence aktuální definice jazyka – bylo by super, kdyby někdo zpracoval definici na úrovni Standard ML (viz stará verze: The Definition of Standard ML - Version 2).

[JS]

No asi nechapu, kde konkretne to setri nejakou lidskou praci. Kazdy mame svou oblibenou matematickou teorii, o tom zadna. Ale pokud tohle ma byt automaticka tvorba kodu, pak je to trochu malo.

[Radek Miček]

Hlavní využití příkazu Auto je při hledání důkazů – tam totiž jde pouze o nalezení termu s odpovídajícím typem a je jedno, jak ten term vypadá. Je tohle odpověď na vaši otázku?

[JS]

Aha, jo, rekl bych, ze ano, dik.

[:::]

Ja jsem si rikal ze tam nikde neni definovany co ta funkce ma delat. Takze to jenom najde nejakou (jakoukoli) funkci ktera splnuje hlavicku? Asi jako bych v C napsal:

int f(int a, int b)

a editor me k tomu doplnil:

{
        return a + b;
}

i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?

[Radek Miček]

i kdyz jsem mohl chtit odcitani, nasobeni, nebo neco slozitejsiho?

Přesně tak. Například, když chci odčítání a použiji typ

binop₁ : ℕ → ℕ → ℕ

tak dostanu

binop₁ a b = b

což není odčítání. Musím tedy upřesnit typ:

binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)

Místo pouhého čísla vracím dvojici. První prvek dvojice je číslo a druhý prvek je důkaz, že první prvek je rozdíl x a y. Odečítání definuji následovně:

_∸_ : ℕ → ℕ → ℕ
m     ∸ zero   = m
zero  ∸ _      = zero
suc m ∸ suc n = m ∸ n

Rovnost vyjadřuji pomocí následujícího typu. Typ je navržen tak, že term refl typu a ≡ b jde zkonstruovat pouze tehdy, jsou-li a a b stejné:

data _≡_ {A : Set} (x : A) : A → Set where
  refl : x ≡ x

Následuje definice závislého páru, kde typ druhé složky závisí na hodnotě první složky:

record Pair (A : Set) (B : A → Set) : Set where
  constructor _,_
  field
    proj₁ : A
    proj₂ : B proj₁

Nastavení parseru:

infixl 6 _∸_
infix  4 _≡_ _,_

Funkce vracející typ (tj. výrok), že rozdíl prvních dvou čísel je roven třetímu číslu:

minus_pred : ℕ → ℕ → ℕ → Set
minus_pred x y res = x ∸ y ≡ res

Pro tento typ už příkaz Auto vygeneruje požadovanou funkci:

binop₂ : (x : ℕ) → (y : ℕ) → Pair ℕ (minus_pred x y)
binop₂ a b = a ∸ b , refl

[Josef Kufner]

Asi mi něco uniká, ale v čem je tato šílenost lepší než prosté napsání "a - b"?

[Radek Miček]

Myslím, že neuniká. V ničem to není lepší. Je to jen příklad, že vlastnost výsledku funkce jde specifikovat typem. V tomto případě to však nemá žádné výhody – spíše naopak.

Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.

[Josef Kufner]

Příklad praktického použití je třeba funkce, která transformuje program a kde chceme, aby výsledný program dával stejné výsledky jako původní program.

Tohle větou jsi měl celý článek uvést

[:::]

Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?

Nebo u binop2 nejde o vygenerovani odcitani, ale o dukaz ze _-_ odpovida minus_pred? Potom by to asi chtelo jeste upravit definici minus_pred aby nepouzival primo _-_.

[Radek Miček]

Vygenerovalo by to neco i kdybych nenadefinoval operator _-_ a minus_pred definoval jinym zpusobem - treba pomoci scitani?

Nejspíš ne.

Konkrétně, pokud máte na mysli podobnou definici

minus_pred : ℕ → ℕ → ℕ → Set
minus_pred x y res = y + res ≡ x

tak ne. Problém je v tom, že pro x < y neexistuje přirozené číslo res a Auto hledá totální funkci (všude definovanou).

Kdybych zadefinoval relaci ≥ a funkci binop₂ definoval pouze pro x ≥ y, tak by to stejně nenašel – je to už příliš složité. Nezkoušel jsem to, ale myslím, že by se muselo nadefinovat ∸, pak dokázat lemma, že z x ≥ y a x ∸ y ≡ res plyne y + res ≡ x, a pak by to našel (ale to už není příliš zajímavé, protože je to vlastně celé hotové).

[csv22]

To use Toto, you must check the recommended list of experts who specialize in verifying the safety of online private Toto. You can trust it only when you sign up for the site using the safety code of an expert who provides the best Sports Toto betting environment. https://bebe41.com

[svsv]

Our Toto site offers high-return dividends to give sports betting enthusiasts the most benefits. And with the highest safety in the private Toto industry, you can freely use Toto, Powerball, and Casino 24 hours a day. We continuously strive to provide the most ideal betting environment. https://sports-totosite.com/%EC%95%88%EC%A0%84%EB%86%80%EC%9D%B4%ED%84%B0

[bddbd]

In order to recommend high-level Toto sites, an odds system managed by experts in the private Toto, Powerball, and Casino fields is operated. Online private Toto, which ranks first in safety, will be able to provide sports betting users with an optimal Toto betting experience. https://mujuru.com/%EC%82%AC%EC%84%A4%ED%86%A0%ED%86%A0%20%EC%9A%B4%EC%98%81%ED%8C%80%EC%9D%98%20%EC%97%AD%EB%9F%89%20%EA%B2%80%EC%A6%9D%EC%9D%B4%20%ED%95%84%EC%9A%94%ED%95%9C%20%EC%9D%B4%EC%9C%A0

[바카라검증사이트]

We are looking for a lot of data on this item. In the meantime, this is the perfect article I was looking for . Please post a lot about items related to 바카라검증사이트 !!! I am waiting for your article. And when you are having difficulty writing articles, I think you can get a lot of help by visiting my .

[파워볼사이트]

I've been looking for photos and articles on this topic over the past few days due to a school assignment, 파워볼사이트 and I'm really happy to find a post with the material I was looking for! I bookmark and will come often! Thanks :D

[바카라사이트]

I've been troubled for several days with this topic. 바카라사이트, But by chance looking at your post solved my problem! I will leave my blog, so when would you like to visit it?

[메이저토토사이트]

Hey, I simply hopped over in your web page by means of StumbleUpon. Not one thing I might in most cases learn, however I favored your feelings none the less. Thank you for making something price reading. 메이저토토사이트

[온라인바카라]

Hello, I read the post well. [url=https://oncasino.biz/]온라인바카라[/url] It's a really interesting topic and it has helped me a lot. In fact, I also run a website with similar content to your posting. Please visit once

[온라인바카라]

Hello, I read the post well. 온라인바카라 It's a really interesting topic and it has helped me a lot. In fact, I also run a website with similar content to your posting. Please visit once

[Charles]

Have a look at amazingly crafted leather Jackets at a discounted price.Mens White Striped Black Leather Jacket

[keo nha cai]

I am very impressed with your writingkeonhacai I couldn't think of this, but it's amazing! I wrote several posts similar to this one, but please come and see!

[바카라사이트]

I have been looking for articles on these topics for a long time. 바카라사이트 I don't know how grateful you are for posting on this topic. Thank you for the numerous articles on this site, I will subscribe to those links in my bookmarks and visit them often. Have a nice day.

[keonhacai]

Hello ! I am the one who writes posts on these topics keo nha cai I would like to write an article based on your article. When can I ask for a review?

[바카라게임사이트]

I'm so happy to finally find a post with what I want. 바카라게임사이트 You have inspired me a lot. If you are satisfied, please visit my website and leave your feedback.

[카지노사이트]

This is the post I was looking for. I am very happy to read this article. If you have time, please come to my site 카지노사이트 and share your thoughts. Have a nice day.

[온라인카지노]

Looking at this article, I miss the time when I didn't wear a mask. 온라인카지노 Hopefully this corona will end soon. My blog is a blog that mainly posts pictures of daily life before Corona and landscapes at that time. If you want to remember that time again, please visit us.

[바카라게임사이트]

As I am looking at your writing, 바카라게임사이트 I regret being unable to do outdoor activities due to Corona 19, and I miss my old daily life. If you also miss the daily life of those days, would you please visit my site once? My site is a site where I post about photos and daily life when I was free.

[카지노사이트]

What a post I've been looking for! I'm very happy to finally read this post. 카지노사이트 Thank you very much. Can I refer to your post on my website? Your post touched me a lot and helped me a lot. If you have any questions, please visit my site and read what kind of posts I am posting. I am sure it will be interesting.

[온라인바카라]

Hello, I am one of the most impressed people in your article. 온라인바카라 I'm very curious about how you write such a good article. Are you an expert on this subject? I think so. Thank you again for allowing me to read these posts, and have a nice day today. Thank you.

[카지노온라인]

I finally found what I was looking for! I'm so happy. 카지노온라인 Your article is what I've been looking for for a long time. I'm happy to find you like this. Could you visit my website if you have time? I'm sure you'll find a post of interest that you'll find interesting.

[baccaratcommunity]

It's really great. Thank you for providing a quality article. There is something you might be interested in. Do you know baccaratcommunity ? If you have more questions, please come to my site and check it out!

[바카라게임사이트]

I'm so happy to finally find a post with what I want. 바카라게임사이트 You have inspired me a lot. If you are satisfied, please visit my website and leave your feedback.

[TECH HELP DESK]

Tech support, short for technical support, is a service that provides assistance to users of technology products, such as computers, smartphones, software applications, and other electronic devices. The goal of tech support is to help users troubleshoot and solve technical problems they may encounter while using their devices or software.

Tech support can be provided in various ways, including phone calls, emails, chatbots, or remote access to a user's computer. The support team may also offer advice on how to optimize the device's performance or provide guidance on how to use specific features of the technology product.

Tech support is crucial in ensuring that users can use their devices and software effectively and efficiently without facing too many challenges.

hotmail down?, contact twitter, google chrome help,

avast com, netgear router, acer support,

roku setup help, snapchat help gmail not working,

garmin express download, call alexa, linksys router setup,

google home setup, norton support, microsoft tech support chat, how to switch apple id on iphone, apple computer support,< hp laptop screen is black,

contact support phone number, at&t problems call netflix, contact netflix, Official Willcraft Website, Official Willcraft Sports Website,

WillCraft, WillCraft Sports,

WillCraft, WillCraft Sports,

cricket bats, bat price, >, total sports shop,

cricket bat dimensions, cricket bat for kids,

willow cricket,

best cricket ball in the world,

[슬롯사이트]

This is the perfect post.슬롯사이트 It helped me a lot. If you have time, I hope you come to my site and share your opinions. Have a nice day.

[OKBet]

This article gives the light in which we can observe the reality. This is very nice one and gives indepth information. Thanks for this nice article online sports betting

[UFAAUTO789]

ufabet789 เว็บแทงบอลที่ใหญ่ และการเงินมั่นคงที่สุด สล็อตออนไลน์ ไม่มีขั้นต่ำ ใช้ทุนน้อย เล่นได้ทุกเกม

[ufa168]

Good day! This post could not be written any better! Reading this post reminds me of my previous room mate! He always kept chatting about this. I will forward this page to him. Pretty sure he will have a good read. Thanks for sharing. ufa168

[BETFLIXSUPERVIP]

A very awesome blog post. We are really grateful for your blog post. combat, law enforcement You will find a lot of approaches after visiting your post. I was exactly searching for. Thanks for such post and please keep it up. Great work.betflik เว็บตรง