A Cayenne nyelv

Kifejezések



Kifejezések

A típusok és kifejezések ugyanazon szintaktikus kategóriába tartoznak a Cayenne-ben, tehát amit elmondhatunk a kifejezésekről az igaz lesz a típusokra is:

type ::= expr

Változók
A változók tekinthetők úgy mint egy kifejezés.

expr ::= varid

Például: x
Alkalmazások
A függvények mint alkalmazás két kifejezésből áll:

expr ::= expr expr

Például: f x
(f x) (g x)
Szintaktikus cukorka
A kényelmesebb használat érdekében az operátorok használhatók infix formában. Ez az operátor precedencia. .

Például: x + y
ugyan az mint (+) x y.

Függvények

Függvény kifejezések lambda kifejezésként szerepelnek. A kötött változónak meg kell adni a típusát.

expr ::= \ (varid :: type) -> expr

Például: \ (x::Int) -> x+1
\ (a :: #) -> \ (x :: a) -> x

Függvény típus

A függvény típus is úgy írható mint egy lambda kifejezés, de itt nem kell ilyen bevezető karakter \. Mivel a Cayenne-ben függő típusok vannak a függvény típus hozzáköt egy változót ami előfordulhat az eredmény típusában.

expr ::= (varid :: type) -> type

Például: (x::Int) -> F x

Szintaktikus cukorka
Ha a változó nem jelenik meg az eredmény típusban , a fuggvény típus úgy írható mint Haskell-ben.

expr ::= type -> type

Például: Int -> Int

Típusok típusa

A típusok típusát igy írjuk: #.

expr ::= #

Adat típusok (sums)

Adat típus egy rendezett cimkézett szumma. A következö képpen írjuk

expr ::= data condef | ...
condef ::= conid type ...
conid ::= varid

Példa: data False | True
Ez egy adattípus két konstruktorral, False and True amiknek van típusa data False | True.

Példa: data C1 | C2 Int | C3 Int Bool
Ez egy adattípus amit nevezzünk T -nek, három konstruktorral, C1 típusa T, C2 típusa Int->T, és C3 típusa Int->Bool->T.

Rekurzív típusok készítéséhez szükség van rekurzív definícióra, ami lentebb kerül bevezetésre.

Megjegyzés: Az adattípus nem vezet be új kötött változókat. Az adattípus konstruktorának nincs speciális státusza.

Konstruktorok

Egy adattípus konstruktorának a használatához meg kell adni a konstruktor nevét valamint a típusát ami hozzá tartozik.

expr ::= conid @ type

Példa: True@(data False|True)
Ez a második konstruktor a típusban data False|True.

Példa: C2@(data C1 | C2 Int | C3 Int Bool)
Ez második konstruktor és a kifejezés típusa Int->(data C1 | C2 Int | C3 Int Bool).

A típus különböző esetekben írható mint _ ha a konstruktor típusa nyílvánvaló a szövegkörnyezetből. Példa: C2@_

Case

A Case kifejezések arra használatosak, hogy alaposan megvizsgáljuk a termék típusának a kifejezéseit. Ennek a formája a következő:

expr ::= case expr of { casearm ; ... }
casearm ::= (conid) -> expr

A case kifejezésben nem kell megadni a konstruktor típusát a mintában.

Példa: case x of { (True) -> False; (False) -> True; }
case y of {
  (C1) -> 0;
  (C2) -> \(x::Int) -> x;
  (C3) -> \(y::Int) -> \(b::Bool) -> y;
}

Szintaktikus cukorka
Ha lambda kifejezés van a minta jobb oldalán, a változó ebben elmozdulhat a mintába és a típusa eldobódik.

Példa:
case y of {
  (C1) -> 0;
  (C2 x) -> x;
  (C3 y b) -> y;
}

Record létrehozás

A Record egy rendezetlen cimkézett produktum. Record értékek a következő szabályoknak megfelelően formálhatók

expr ::= struct { [modifier] defn ; ... }
defn ::= labelid :: type = expr
labelid ::= varid

A record korlátlan számú komponenst tartalmazhat. Minden egyes komponensnek van egy cimkéje, egy típusa és egy értéke. A cimke azonosítók a rekord konstrukción belül kötöttek, de kívül kötetlenek. A kötések kölcsönösen rekurzívak.

Rengeteg szintaktikus cukorka van a rekordokban a definíciókra.

Megj: a struct szó kihagyható amikor a szerkezet szabályt nem használom.

Record módosítók
Az egyes rekord komponenseknek lehetnek módosítóik amik hatással vanak a megjelenésükre modifier ::= abstract | concrete | public | private

Példa:
struct { x :: Int = 5; y :: Int = 4; }
struct { idInt :: Int->Int = \ (x::Int) -> x; two :: Int = idInt 2; }
struct { private x :: Int = 2+5; x2 :: Int = x*x; }
struct { concrete c :: Int = 2; inc :: Int->Int = \(x::Int)->x+1; }

Szintaktikus cukorka
A rekord konstrukció elejére téve egy ilyen módosítót az alapértelmezett láthatósági mód megváltozik az adott értékre.

Példa: concrete struct { x::Int=5; y::Int=7; }

Record kiválasztás

Record kiválasztás egy infix `.' használható a kifejezés és a cimke között.

expr ::= expr . labelid

Példa: r.x

Record típusok (products)

A rekord típus jelölése hasonlít a rekord létrehozásánál mutatottra. Az egyetlen különbség az , hogy az absztrakt komponensekre a kifejezés rész elhagyódik és nincsennek módosítók.

expr ::= sig { varid :: type [ = expr ] ; ... }

A sig elhagyható amikor a layout szabályt nem használjuk.

Példa (a rekordok típusa fentebb):
sig { x :: Int; y :: Int; }
sig { idInt :: Int->Int; two :: Int; }
sig { x2 :: Int; }
sig { c :: Int = 2; inc :: Int->Int; }

A rekord típus sajátossága, hogy nem csak az egyes komponensek típusát tartalmazza hanem néha az értéket! Ez arra használatos, hogy elkészítsük egy adat típus konstruktorát egy mudul szignaturája ismerete alapján (=record).

let kifejezések

Cayenne Haskell stílusú let kifejezéseket használ lokális kötések létrehozására.

expr ::= let defn; ... in expr

A kifejezés
let d1; d2; ... in e
szemantikailag ekvivalens a
struct { d1; d2; ...; r::t = e; }.r
ahol r egy új azonosító és t pedig e -nek a típusa.

open kifejezések

Az open kifejezések egy kényelmes megoldást adnak arra, hogy egy rekord több komponensét is elérjük.

expr ::= open expr use varid :: type [ = varid ], ... in expr

A kifejezés
open e use i1::t1=i1', i2::t2=i2', ... in e'
szemantikailag ekvivalens
let i1::t1 = e.i1'; i2::t2 = e.i2'; ... in e'

Ha a második varid elhagyom feltételezi azt, hogy ugyan az mint az első. A típus elhagyható. Tehát elég annyit írnom, hogy
open e use i1, i2, ... in e'

Szintaktikus cukorka
A típusok a kifejezések use részében mindíg elhagyhatók.

do kifejezések

Hogy egyszerűbb legyen a monádok használata Cayenne-nek van egy do jeleölési módja a Haskell-hez hasonlóan. A külömbség pedig az , hogy a monádokat expliciten kell megadni.

expr ::= do expr { bind ; ... }
bind ::= varid :: type <- expr | expr

A do jelölés így terjeszkedik

do expr { binds }
--->
open expr use (>>=), (>>), return in T { binds }

És a fordítás

T { expr } ---> expr
T { expr ; binds } ---> expr >> T { binds }
T { arg <- expr ; binds } ---> expr >>= \ arg -> T { binds }

Példa:

do System$IO.Monad {
    s :: String <- readFile "foo";
    writeFile "bar" s;
}
Példa
Egy record (modul) boolean -ekre. 
struct {
  Bool :: # = data False | True;
  True :: Bool = True@Bool;
  False :: Bool = False@Bool;
  not :: Bool -> Bool = \ (x::Bool) ->
    case x of {
    (False) -> True;
    (True) -> False;
    };
}

Természetes számok:
17:52 2009.06.28. 

struct {
  Nat :: # = data Zero | Succ Nat;
  add :: Nat -> Nat -> Nat = \ (x::Nat) -> \ (y::Nat) ->
    case x of {
    (Zero) -> y;
    (Succ n) -> Succ (add n y);
  };
}

Egyenlőség bizonyítások

Cayenne -ben van egy szintaktikus cukorka, hogy az egyenlőség bizonyítás készítése egyszerűbb és olvashatóbb legyen.

expr ::= [ expr ]
expr ::= expr { eqstep ... }
eqstep ::= ={ DEF }= expr eqstep ::= ={ expr }= expr