Típus, típuslevezetés, típusoperátor

14.1. Kérdés.

A -> típusoperátor merre köt? Jobbra vagy balra?

14.1. Válasz.

Oktató: Jobbra köt.

14.2. Kérdés.

Egy kérdésem lenne a zéhá 6.c feladatáról: a feladat a fun f x y = y (x y) típusának a levezetése.

Én úgy gondolkoztam, hogy mivel az x függvény argumentumul kapja y-t, amely szintén függvény, ezért ('a -> 'b) -> 'a lesz az x típusa, eddig a helyes megoldás is ilyen. De ezután ebből egy olyan függvény lesz, amely 'b típust ad eredményül (az y miatt), de az argumentuma egy függvény (x y), és ezért ('b -> 'a ) -> 'b.

Tehát szerintem az egész : (('a -> 'b) -> 'a) -> ('b -> 'a) -> 'b, ami nyilván nem jó, mert begépeltem az ML értelmezőnek is... :(

val ('a, 'b) f = fn : (('a -> 'b) -> 'a) -> ('a -> 'b) -> 'b

Hol tévedtem?

14.2. Válasz.

Oktató: A függvény törzsében (az egyenlőségjel utáni részben) az y argumentuma nem az x függvény, hanem az x függvény y-ra való alkalmazásának az eredménye, amit 'b-val jelölt. Éppen innen kellett volna elindulnia: az y-t alkalmazzuk valamire (jelöljük a típusát 'a-val), az eredményét pedig 'b-val: y : 'a -> 'b. Ezután az x-et az y-ra alkalmazzuk, az eredménye pedig ugyancsak az y-nak (egy másik példányának) lesz az argumentuma, tehát az x eredményének és az y argumentumának azonos típusúaknak kell lenniük: x: ('a -> 'b) -> 'a. Összeállt minden, már csak be kell írni a dolgokat (a bal oldal alapján, figyelembe véve, hogy az egyenlőségjel mindkét oldalán azonos típusú értékeknek kell lenniük):

f: (('a -> 'b) -> 'a) -> ('a -> 'b) -> 'b

Figyelem: a zárójelek most fontosak! Az mosml válasza is ezt tükrözi.

14.3. Kérdés.

Ha jól gondolom, egy SML típuskifejezésben a * típusoperátor a -> típusoperátornál erősebben és ráadásul balra köt. Jól gondolom?

14.3. Válasz.

Oktató: Abban igaza van, hogy erősebben köt, és másképp, mint a jobbra kötő -> típusoperátor. De abban téved, hogy balra kötne - ugyanis se nem jobbra, se nem balra nem köt. Ezt illusztrálják az alábbi példák:

(1,2,3) : (int * int) * int;
(1,2,3) : int * (int * int);

amelyeket az mosml hibásnak talál:

! (1,2,3) : (int * int) * int;
! ^
! Type clash: expression of type
!   int * int * int
! cannot have type
!   (int * int) * int
- ! Toplevel input:
! (1,2,3) : int * (int * int);
! ^
! Type clash: expression of type
!   int * int * int
! cannot have type
!   int * (int * int)

Ha a * balra vagy jobbra kötne, a kettő közül az egyik zárójelezést jónak tartaná.

Persze nyilvánvaló módon nem fogadhatja el az mosml egyiket sem, ui. az (int * int) * int egy olyan pár típusa, amelynek az első tagja maga is egy pár, az int * (int * int) pedig egy olyan pár típusa, amelynek a második tagja maga is egy pár. Ezzel szemben az int * int * int egy hármas típusa.

14.4. Kérdés.

Valaki árulja el nekem, legyen oly szíves, hogy hogyan kell levezetni az alábbi függvény típusát.

fun f p q r s = p(q r s);

14.4. Válasz.

Oktató: No, akkor nézzük! Amint látjuk, az r és az s típusáról semmi nem derül ki, ezért jelöljük a típusokat egy-egy típusváltozóval:

r = 'a
s = 'b

A q függvény egy részlegesen alkalmazható függvény r és s argumentumokkal. Valamit varázsol, és visszaad valamilyen típusú értéket; mivel erről sem tudhatjuk, hogy milyen típusú, jelöljük 'c-vel. Így a q függvény típusa:

q = 'a->'b->'c

A p-ről az látszik, hogy egy paramétere van, méghozzá a q r s függvényalkalmazásnak, vagyis a q függvény két paraméterrel történő meghívásának az eredménye. A q-ról tudjuk, hogy 'c típusú értéket ad eredményül, így a p függvény értelmezési tartományát a 'c típusú értékek alkotják. Az, hogy ebből a p milyen típusú eredményt állít elő, megintcsak nem derül ki, jeöljük hát 'd-vel. Így:

p = 'c -> 'd

Most már, hogy a p, q, r és s típusát is meghatároztuk, összerakhatjuk az f függvény típusát:

f  = ('c -> 'd) -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'd

Még egyszer, rövidebben: Mivel az s és az r argumentumok tetszőleges típusúak lehetnek, legyen az r 'a, az s 'b típusú. A q függvény, mégpedig olyan, amely r-re alkalmazva függvényt ad eredményül, amely azután s-ből állít elő valamit, legyen ennek típusa 'c. Tehát q: 'a -> ('b -> 'c), de a zárójel elhagyható, mivel a -> jobbra köt. A p olyan függvény, amely a q r s értékéből állít elő valamit, legyen a típusa 'd, tehát p: 'c -> 'd. Az f olyan függvény, amely p-re alkalmazva olyan függvényt ad, amely q-ra alkalmazva olyan függvény ad, amely r-re alkalmazva s-ből állít elő 'd típusú értéket. Tehát f típusa:

('c -> 'd) -> (('a -> ('b -> 'c)) -> ('a -> ('b -> 'd)))

és a felesleges zárójelek elhagyása után:

('c -> 'd) -> ('a -> 'b -> 'c) -> 'a -> 'b -> 'd

Egyszerű, nem?

A kérdező folytatja: Oké, tényleg egyszerű, csak azt honnan lehet tudni, hogy mind az s, mind az r paraméter (argumentum)? r miért nem részlegesen alkalmazható függvény? Ha pl. fun f x y z = y x z, akkor ebben mind az x, mind a z egyszerűen paraméter, és az x nem részlegesen alkalmazható függvény?

Oktató: Onnan tudható, hogy melyik név áll függvényalkalmazási-pozícióban, és melyik nem. A függvényalkalmazás a lehető legerősebben kötő művelet, a kiértékelés (hacsak zárójelek vagy precedenciák nem módosítják) mindig balról jobbra halad. A függvény nevét az argumentumtól egy vagy több szeparátor (formázó karakter vagy kerek nyitó zárójel) választja el. (A vessző, pontosvessző nem szeparátor!)

Nézzük még egyszer a kérdéses függvényt:

fun f p q r s = p(q r s);

Az érthetőség kedvéért tegyük ki a zárójeleket a deklaráció mindkét oldalán (az alábbi deklarációt az mosml nem tudná kiértékelni, mert a nyelv szintaxisa nem engedi meg, hogy a deklaráció bal oldalán a deklarálandó nevet zárójelbe tegyük):

fun (((f p) q) r) s = (p ((q r) s))

Tudjuk, hogy minden függvény egyargumentumú az SML-ben. Függvény az, amelynek van argumentuma. A fenti deklarációban tehát a következő dolgok jelölnek függvényt:

• f p q r, argumentuma: s
• f p q, argumentuma: r
• f p, argumentuma: q
• f, argumentuma: p
• q r, argumentuma: s
• q, argumentuma: r
• p, argumentuma: (q r) s !!!

A nevek közül tehát f, q és p jelölnek függvényt (pontosabban róluk tudjuk, hogy függvényt kell jelölniük), a többi nem függvényt jelöl (pontosabban róluk nem tudjuk, hogy milyen értéket jelölnek, akár függvényértéket is jelölhetnek). Világos?

14.5. Kérdés.

Valaki legyen szíves és segítsen nekem megérteni, hogy a

fun f v = v o map

típusa miért az, ami.

14.5. Válasz.

Oktató: Az o infix operátor a függvénykompozíció műveleti jele az SML-ben: jobb oldali 'd -> 'e és bal oldali 'e -> 'g típusú operandusából állít elő egy 'd -> 'g típusú függvényt. (A 'd, 'e, 'g jelöléseket addig használom, amíg nem tudok meg róluk többet.) A jelen esetben a szereposztás az, hogy a map van az o jobb oldalán, tehát neki kell d' -> 'e típusúnak lennie (az map eredménye a v paramétere). A map típusa ('a -> 'b) -> ('a list -> 'b list), ezért

'd = 'a -> 'b
'e = 'a list -> 'b list

A 'g-ről nem tudunk semmi közelebbit. v típusa ('e -> 'g), behelyettesítve ('a list -> 'b list) -> 'g, v o map típusa pedig 'd -> 'g, behelyettesítve ('a -> 'b)->'g. Így az f típusa:

(('a list -> 'b list) -> 'g) -> (('a -> 'b)->'g)

A felesleges zárójeleket elhagyhatjuk, és g-t a megszokottabb 'c-re cserélhetjük:

(('a list -> 'b list) -> 'c) -> ('a -> 'b) -> 'c

14.6. Kérdés.

A kérdés, amelyet Tóth kolléga helyezett a listára, a következő:

fun f a a b = a b

Mi ennek a szépségnek a típusa?

Nos, én kidolgoztam egy módszert a típuslevezetésre, de az itt nem működik. Miért nem? Nem tudom. :( Az mosml az alábbi válasszal áll elő:

'a -> ('b -> 'c) -> 'b -> 'c

Megpróbálom most visszafejteni a dolgokat. Tehát a jobb oldal 'c típusú eredményt ad, a b típusára pedig azt mondja, hogy az simán 'b. Ekkor az a típusa nem más, mint 'b -> 'c.

Ezt kitűnően reprezentálja a zárójeles kifejezés. DE! Hát előtte is van egy a, annak miért nem a megállapított típusát írja ki az mosml??? Az én módszerem ezt adja:

('b -> a) -> ('b -> 'a)-> 'b -> 'a

A kérdés: miért nem ezt írja ki az mosml??? Még egy darab mókás mozzanatot engedek meg ezen a helyen: mosml barátunk szerint az alábbi két függvénynek ugyanaz a típusa:

fun f c a b = a b;
fun f a a b = a b;

Ez aztan megváltoztatja a szemléletemet! Azt kell mondjam, hogy az mosml valamit máshogy csinál, mert amíg a

fun f c a b = a b;

deklarációnak nyilvánvaló a levezetése, és az alábbi eredményre vezet:

val ('a, 'b, 'c) f = fn : 'a -> ('b -> 'c) -> 'b -> 'c

addig a

fun f a a b = a b;

deklarációra nem ugyanazt a választ kellene adnia, pedig ugyanazt adja:

val ('a, 'b, 'c) f = fn : 'a -> ('b -> 'c) -> 'b -> 'c

Szerintem ezt még kell vesézni.

14.6. Válasz.

Oktató: Ebben a dologban az a (szerintem csúnya) trükk, ahogyan az mosml értéket köt egy névhez. Mint ismeretes, egy névhez többször is lehet értéket kötni, és az mosml, amikor egy kifejezést kiértékel, nem a nevet, hanem a névhez éppen akkor kötött értéket építi be az eredménybe. Például:

- val a = 1;
> val a = 1 : int
- fun f () = a;
> val f = fn : unit -> int
- f ();
> val it = 1 : int
- val a = 2;
> val a = 2 : int
- f ();
> val it = 1 : int

Azaz az f () eredménye nem változik meg attól, hogy az a név később már más értéket jelöl.

Mivel az SML-ben (a Prologgal ellentétben!) nincs egyesítés, csak behelyettesítés van, a bal oldalon kétszer is előforduló a argumentum valójában két, egymástól független argumentumot jelöl! Nézzünk egy nagyon egyszerű esetet és az mosml válaszát:

- fun f a a = 1;
> val ('a, 'b) f = fn : 'a -> 'b -> int

Ezért ekvivalens a fun f a a b = a b függvénydeklaráció típusa a fun f x a b = a b függvénydeklaráció típusával. Az utóbbi esetben az f típusának a levezetése feltehetőleg már senkinek nem jelent nehézséget.

Következő példaként nézzük az f két alkalmazását mosml alatt:

- fun f a a b = a b;
> val ('a, 'b, 'c) f = fn : 'a -> ('b -> 'c) -> 'b -> 'c
- f chr (fn x => x + 5) 3;
> val it = 8 : int
- f (fn x => x + 5) chr 3;
> val it = #"\^C" : char

Jól látszik, hogy az f első argumentumával a kutya se törődik. A helyzet fokozható: :-)

- fun f a a a a a b = a b;
> val ('a, 'b, 'c, 'd, 'e, 'f) f = fn :
  'a -> 'b -> 'c -> 'd -> ('e -> 'f) -> 'e -> 'f

Az SML-ben egy függvénynek nem lehetnének azonos nevű paraméterei! Tekintsük úgy, hogy ez egy hiba az mosml-ben. Az smlnj korrekt módon viselkedik:

Standard ML of New Jersey v110.42 [FLINT v1.5], Oct 16, 2002
- fun f a a b = a b;
stdIn:1.5-1.18 Error: duplicate variable in pattern(s): a

Haladóknak. Aki az eddigieket csak többé-kevésbé értette, már ne figyeljen ide! Érdekes módon az mosml szerint a fun f a a b = a b deklaráció típusa már nem ekvivalens a fun f a x b = a b deklaráció típusával, ugyanis az előbbié 'a -> ('b -> 'c) -> 'b -> 'c, míg az utóbbié ('b -> 'c) -> 'a -> 'b -> 'c. (Az, hogy az mosml az utóbbira nem betű szerint ezt írja ki, ne tévesszen meg senkit: a típusváltozók neve - feltéve, hogy az azonosak helyébe azonosakat írunk - tetszőleges más névre lecserélhető). Ennek oka a kifejezések kiértékelési sorrendjében keresendő.

14.7. Kérdés.

Ha valakinek van kedve és ideje, leírná nekem, hogy hogyan kapjuk meg az f típusát az alábbi deklaráció esetén?

fun f (v, a) = map o (v a)

14.7. Válasz.

Oktató: A feladat nem egyszerű. Szerncsére nemrég volt egy hasonló kérdés, ezért most a magyarázat lehet tömör. Az o a függvénykompozíció művelete, típusa ('e -> 'g) * ('d -> 'e) -> 'd -> 'g.

A map, típusa ('a -> 'b) -> ('a list -> 'b list), az o bal oldalán van, ezért ('e -> 'g) = ('a -> 'b) -> ('a list -> 'b list), és így e' = ('a -> 'b) és 'g = ('a list -> 'b list).

Az o jobb oldalán a v a van, ezért a típusának 'd -> 'e-nek kell lennie. Az a-ra semmilyen megkötés nincs, jelöljük a típusát 'c-vel. A v típusa tehát: 'c -> ('d -> 'e).

A megfelelő helyre behelyettesítve, amit csak lehet, kapjuk az f típusát:

f : ('c -> ('d -> 'e)) * 'c -> ('d -> 'g)
f : ('c -> ('d -> ('a -> 'b))) * 'c ->
                                ('d -> ('a list -> 'b list))

A típusnevek szisztematikus cseréjével és a felesleges zárójelek elhagyásával azt kapjuk, amit az mosml is kiír (azért, hogy a régi és az új típusnevek ne keveredjenek, az új típusneveket nagybetűvel írjuk):

f: ('A -> 'B -> 'C -> 'D) * 'A -> 'B -> 'C list -> 'D list

14.8. Kérdés.

Mi lesz a típusa? Miért??

fun f r s f = f(r, s)

Valami átírásféle... Volt ma az órán ilyesmi, de mi ennek a megoldása?

14.8. Válasz.

Oktató: Először is jó tudni, hogy a két f-nek a fun és az = között - a függvénynévnek és az argumentumnévnek - semmi közük egymáshoz! Ha az argumentumot átnevezzük, a függvény jelentése nem változik meg. Első látásra nem tudható, hogy az = jobb oldalán az f vajon az argumentumként átadott függvény alkalmazását vagy az éppen most definiált függvény rekurzív alkalmazását jelenti-e. De ha jobban szemügyre veszük a definíciót, nyilvánvalóvá válik, hogy az utóbbiról nem lehet szó, mert a deklaráció két oldalán az f kétféleképpen lenne paraméterezve. Ezért az eredeti definíció a következővel ekvivalens:

fun f r s g = g(r, s)

Ettől kezdve már könnyű dolgunk van: r és s típusáról semmit nem tudunk, jelöljük ezeket 'a-val, illetve 'b-val. g-nek olyan függvénynek kell lennie - ez a definíció jobb oldalából tudható -, amely egy 'a *'b típusú értékből egy 'c típusú értéket ad eredményül. 'c-ról ennél többet nem tudunk meg. f-et részlegesen alkalmazható függvény neveként deklaráltuk, ezért a típusa ez (megjelölve, hogy a típuskifejezés összetevői honnan származnak):

'a -> 'b -> ('a * 'b -> 'c) -> 'c
 |     |           |            |
 v     v    \---v---/     v
 r     s           g            f eredménye

14.9. Kérdés.

Ha egy listából, amelynek az elemei listák, szeretnék egy olyan listát csinálni, amelynek az elemei az eredeti elem-listák elemei, akkor mi is a megoldás?

14.9. Válasz.

Oktató: A List.concat függvény, amely például így definiálható:

fun concat lss = foldr op@ [] lss;

Haladóknak. Azt tanultuk, hogy a részlegesen alkalmazható függvények formális paraméterei jobbról balra haladva elhagyhatók a definíció mindkét oldalán. Az előző definíciónak ennek értelmében ekvivalensnek kell lennie a következővel:

val concat = foldr op@ [];

Az mosml próbálkozásunkat egy figyelmeztetéssel honorálja:

- val concat = foldr op@ [];
! Warning: Value polymorphism:
! Free type variable(s) at top level
!   in value identifier concat
> val concat = fn : 'a list list -> 'a list

Amikor először alkalmazzuk ezt a concat függvényt, az mosml újra figyelmeztet:

- concat [[1,2],[3,4,5]];
! Warning: the free type variable 'a
! has been instantiated to int
> val it = [1, 2, 3, 4, 5] : int list

Ettől kezdve a concat többé már nem polimorf:

- concat [[1.2],[3.4,5.0]];
! Toplevel input:
! concat [[1.2],[3.4,5.0]];
!          
! Type clash: expression of type
!   real
! cannot have type
!   int

De ha a concat-ot a korábbi definícióval hozzuk létre, a polimorf jellegét nem veszíti el:

- fun concat lss = foldr op@ [] lss;
> val 'b concat = fn : 'b list list -> 'b list

- concat [[1,2],[3,4,5]];
> val it = [1, 2, 3, 4, 5] : int list
- concat [[1.2],[3.4,5.0]];
> val it = [1.2, 3.4, 5.0] : real list

A magyarázatot az ún. értékpolimorfizmus adja meg, amelyről az FP-GYIKPolimorfizmus c. fejezetében valamivel többet, az ott hivatkozott leírásokban és a szakirodalomban sokkal többet olvashatnak az igazán haladók.

14.10. Kérdés.

El tudná mondani valaki, hogy az alábbi kifejezésben mi az x típusa?

val x = let val xs = List.filter Char.isAlpha [#"1", #"3"]
        in xs
        end

14.10. Válasz.

Oktató: filter : ('a -> bool) -> 'a list -> 'a list, azaz ha átad neki egy ('a -> bool) típusú predikátumot (olyan függvényt, amelynek bool típusú az eredménye), kiválogatja az 'a list típusú listából azokat az elemeket, amelyekre a predikátum igaz, és az elemek eredeti sorrendjét megőrző, ugyancsak 'a list típusú listával tér vissza. A feladatban a predikátum Char.isAlpha : char -> bool és [#"1",#"3"] : char list a lista, amelyre filter a predikátumot alkalmazza. Char.isAlpha betűre igaz, egyébre hamis értékkel tér vissza: mivel az argumentumlistában nincsenek betűk, xs a [] : char list értéket kapja a let-kifejezésben, amelynek maga xs az eredménye. Végül a külső deklaráció az x a let-kifejezés eredményét, azaz xs értékét köti x-hez.

14.11. Kérdés.

Meg tudná mondani valaki, hogy az alábbi kifejezésben mi az x típusa? Nekem nem megy. :( Úgy tűnik, hogy az xs bevezetése csak megtévesztés, hiszen a végén x-nek xs lesz az értéke!

  val x = let val xs = List.find not [false, true] in xs end

A List.find eljárás a false értéket adja vissza, mert arra teljesül a not függvény, tehát az xs értéke (és ezáltal x is) false. Nem? Akkor most az x bool típusú?

14.11. Válasz.

Hallgató: Az sml-jegyzet szerint (ld. a függelékében) az van, hogy a List.find, amikor olyan listaelemet talál, amelyre az alkalmazott - itt not - függvény igaz eredményt ad, akkor a SOME v (ahol v a talált elem) eredményt adja. Ha nem talált volna ilyet, akkor NONE-t ad vissza. Namost, SOME típusa 'a option, tehát a válasz a feltett kérdésre: x = false : bool option.

Oktató: Az xs bevezetése valóban felesleges (nevezhetjük megtévesztésnek is), hiszen

let val xs = List.find not [false, true] in xs end =
                                  List.find not [false, true]

A hallgatói válasz helyes: x értéke false, a típusa pedig bool option, de a magyarázat nem elég pontos. -- Az előadáson a datatype deklarációt és az Option könyvtárat tárgyaljuk, az alábbi válasz ezek ismeretében válik világossá.

List.find típusa és alkalmazásának eredménye, továbbá SOME és NONE típusa helyesen a következő.

List.find : ('a -> bool) -> 'a list -> 'a option

Ha a List.find-ot egy 'a -> bool típusú p predikátumra alkalmazzuk, akkor olyan függvényt ad eredményül, amelyet egy 'a típusú elemekből álló xs listára alkalmazhatunk. Ha a List.find p xs kifejezésben az xs-nek nincs a p-t kielégítő eleme (azaz olyan eleme, amelyre p-t alkalmazva true eredményt kapnánk), akkor NONE lesz a függvényalkalmazás eredménye. Ha az xs-nek van egy vagy több p-t kielégítő eleme, akkor - az xs balról számított első ilyen elemét x-szel jelölve - az eredmény SOME x lesz.

• a SOME ún. adatkonstruktorfüggvény, a típusa: 'a -> 'a option,
• a NONE ún. adatkonstruktorállandó, a típusa: 'a option.

14.12. Kérdés.

Sziasztok, egy kis segítségre lenne szükségem. A kérdés: miért ez az f típusa?

fun f (x, y) = y(x+1, 2.0)
     Megoldás: int * (int * real -> 'a) -> 'a

Szóval miért ez a megoldás? Meg egyébként is hogy kell az ilyet általánosságban megoldani?

14.12. Válasz.

Oktató: Az y-t az (x+1, 2.0)-ra alkalmazzuk, ezért mivel az x int típusú (mert hozzá tudjuk adni az int típusú 1-et), a 2.0 pedig real típusú, az y-nak int * real az argumentuma, az eredménye pedig ismeretlen típusú, jelöljük 'a-val. Az y alkalmazásának eredménye egyúttal az f alkalmazásának az eredménye, tehát az f típusa:

f : int * (int * real -> 'a) -> 'a

A kérdező folytatja: És ebben a feladatban miért ez az f típusa?

fun f x y z = x z y
     Megoldás: ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

Oktató: A deklaráció jobb oldalából látható, hogy csak az x van függvényalkalmazási pozícióban, z és y a részlegesen alkalmazható x paraméterei. A paraméterek és az x eredményének típusát, mivel nem tudunk róluk többet, jelöljük típusváltozókkal:

z : 'a
y : 'b
x : 'a -> 'b -> 'c

A részekből már könnyű összerakni az egészt, figyelembe véve, hogy f is részlegesen alkalmazható függvény:

f : ('a -> 'b -> 'c) -> 'b -> 'a -> 'c

A kérdező folytatja: Már csak egy kérdésem maradt: mi az f típusa a következő definíció után?

fun f x y = y(x y)
     Megoldás: (('a -> 'b) -> 'a) -> ('a -> 'b) -> 'b

Oktató: Nem győzöm elégszer hangsúlyozni, hogy a típusegyenletek megoldásakor mindig a deklaráció jobb oldalát kell először szemügyre venni. A legfontosabb, hogy megállapítsuk, melyik név van függvényalkalmazási pozícióban.

Ebben a feladatban mind y első előfordulása az = jobb oldalán, mind x függvényalkalmazási pozícióban van, az x függvény paramétere y, az y függvény paramétere pedig az x y függvényalkalmazás eredménye.

A típusokról semmi konkrétumot nem tudunk meg, ezért az y típusa a lehető legspecifikusabban így írható fel: 'a -> 'b. Ha ez megvan, már rutinfeladat a levezetés:

x : ('a -> 'b) -> 'a

Az eredménynek 'a típusúnak kell lennie, mert az y-t alkalmazzuk rá! Végül behelyettesítve és kirakva a zárójeleket, ahol szükséges:

f : (('a -> 'b) -> 'a) -> ('a -> 'b) -> 'b

14.13. Kérdés.

Meg tudná valaki mondani, hogy ennek mi a típusa:

val x = map (foldl op<> (3<>4))

14.13. Válasz.

Hallgató: A foldl op<> függvény egy 3<>4 = false értékű, bool típusú egységelemmel kezdve szépen összehasonlítgatja egymás után egy lista elemeit (ezek is csak bool típusúak lehetnek, hogy működjön az op<>), ennek tehát egy lista az argumentuma, és bool típusú a végeredménye. Viszont ott van előtte a map, amely miatt az egész egy bool list típusú listákból álló listára alkalmazható, és a végeredménye a részlisták eredménye egy listába fűzve. Azaz: bool list list -> bool list.

Szóljatok, ha valami nem stimmel, vagy nem érthető...

Másik hallgató: Megfogalmazom másképpen, formálisabban, hátha valakinek segítek vele. A 3 <> 4 = false, a típusa bool, ez az ún. egységelem (trükkös). Ebből következően a op <> bool * bool -> bool típusú ebben a feladatban. Tehát a listának, amelyre az x-et alkalmazzuk, bool list-nek kell lennie. Ezért

foldl op<> (3<>4) : bool list -> bool

A map típusa:

map : ('a -> 'b) -> 'a list -> 'b list =
                           ('a -> 'b) -> ('a list -> 'b list)

Itt most 'a = bool list és 'b = bool, és ezért

x : bool list list -> bool list

14.14. Kérdés.

Írjon az alábbi fejkommentet kielégítő SML-függvényt! Segítségül példát is mutatunk az alkalmazására.

(* nthFmBehind(i, xs) = xs hátulról számított i-edik eleme,
        ahol egy lista utolsó elemének a sorszáma 1
        PRE: i > 0
   nthFmBehind : (int * 'a list) -> 'a
*)

Példa: nthFmBehind (3, ["w","x","y","z"]) = "x"

Ehhez a feladathoz kérek segítséget. A probléma az, hogy ha nem kezelem le az xs = [] esetet, akkor nem enged tovább, ha lekezelem, akkor viszont a visszaadott érték nem megfelelő, hiszen nem tudom visszaadni a listabeli elem típusát. Mi a megoldás?

14.14. Válasz.

Hallgató: Itt van egy megoldásom:

fun nthFmBehind (i, xs) =
      let
          val j = length xs - i
          fun s (0, (y::ys)) = y
            | s (n, (y::ys)) = s(n-1, ys)
      in
         s(j, xs)
      end;

Példa:

- nthFmBehind (3, ["w","x","y","z"]);
> val it = "x" : string
- nthFmBehind (5, ["w","x","y","z"]);
! Uncaught exception:
! Match
- nthFmBehind (1, []);
! Uncaught exception:
! Match

Oktató: A hallgató megoldása elfogadható, de nem szép benne, hogy az s segédfüggvény nem kezel minden esetet, amire az mosml figyelmeztet is.

! Toplevel input:
! ..............s (0, (y::ys)) = y
!             | s (n, (y::ys)) = s(n-1, ys)
! Warning: pattern matching is not exhaustive

A korrekt megoldásnak minden esetet kezelnie kell, az üres listára pedig kivételt (exception) kell jeleznie. Ez lehet a hasonló esetekben jelzett Empty (vö. List.hd, List.tl), esetleg a Subscript (vö. List.nth, List.take, List.drop), vagy egy erre a célra deklarált saját kivételnév. Egyébként kivételt jelez a hallgató megoldása is, de a Match hibaüzenet szerintem nem elég kifejező az adott esetben.

Gyorsan megírható az a változata, amely az i = 0 és az i > length xs speciális eseteket is automatikusan kezeli, ha a List.nth : 'a list * int -> 'a és a length : 'a list -> int függvényeket alkalmazzuk. List.nth alkalmazásához tudni kell, hogy a lista fejének (bal szélső elemének) 0 az indexe.

fun nthFmBehind (i, xs) = List.nth(xs, length xs - i);

Példa:

- nthFmBehind (3, ["w","x","y","z"]);
> val it = "x" : string
- nthFmBehind (5, ["w","x","y","z"]);
! Uncaught exception:
! Subscript
- nthFmBehind (1, []);
! Uncaught exception:
! Subscript

Kifejezőbbek lesznek a hibaüzenetek, ha az üres listára is írunk egy klózt:

fun nthFmBehind (_, []) = raise Empty
  | nthFmBehind (i, xs) = List.nth(xs, length xs - i);

Példa:

- nthFmBehind (3, ["w","x","y","z"]);
> val it = "x" : string
- nthFmBehind (5, ["w","x","y","z"]);
! Uncaught exception:
! Subscript
- nthFmBehind (1, []);
! Uncaught exception:
! Empty

Ugyancsak gyorsan megírható az a változata, amely a List.nth mellett a rev-et alkalmazza.

fun nthFmBehind (_, []) = raise Empty
  | nthFmBehind (i, xs) = List.nth(rev xs, i-1);

Végül következzen egy olyan változata, amely a List.nth függvényt nem alkalmazza.

fun nthFmBehind (_, []) = raise Empty
  | nthFmBehind (i, xs) =
      let fun nFmB (0, z::zs) = z
            | nFmB (i, _::zs) = nFmB(i-1, zs)
            | nFmB (_, []) = raise Subscript
      in
          nFmB(i-1, rev xs)
      end;

A két utóbbi megoldás esetén az mosml válaszai az előző példában bemutatottakkal azonosak lesznek.

14.15. Monológ.

Hallgató: Azért írom az info2000-re is, mert azt többen olvassák. Biztos sok hülyeséget is írok, és nem teljesen korrekt a nyelvezet, de remélem, mindenkinek hasznára lesz, legalábbis a zhig :)! Ha tetszik a dolog, tegyétek fel az infositera is! Típuslevezetéses feladatokat valahogy így lehet megoldani:

1. Vegyük az alábbi példát. Saját függvényt definiálunk.
   fun valami x = x;
   
   Ennek típusa: 'a -> 'a.

   A 'a, 'b, 'c stb. tetszőleges típust jelölnek, típusváltozóként foghatók fel, kb. úgy, mint a C++ban a template. A típuslevezetést úgy kapjuk meg, hogy a rendszer felteszi, hogy x-nek 'a típusa van, ekkor viszont a válasz is 'a típusú, hiszen pontosan x-et adja vissza a függvény. A -> jel a leképzés jele, bal oldalán a függvény argumentumának, jobb oldalán a függvény által visszaadott értéknek a típusa latható. Ez a függvény tehát alkalmazható tetszőleges típusú paraméter esetén, és ugyanolyan típusú értéket ad vissza.

2. Vegyünk egy olyan példát, amelyben egy ennes szerepel:
   fun valami (x, y) = x;
   
   Ennek típusa: 'a * 'b -> 'a

   A * jel a típuskifejezésben az enneseket jelöli (egyébként a direktszorzat jelét akarja sugallni), és erősebben köt, mint a ->, tehát a kifejezés így értelmezendő:

   'a * 'b -> 'a
   
   Egy 'a és egy 'b típusú értékekből álló párt képezünk le egy 'a típusú értékre.

3. Vegyünk egy olyan példát, amelyben egy lista szerepel:
   fun valami (fej::farok) = fej;
   
   Ennek a típusa: 'a list -> 'a

   Itt a list típusoperátor az új: egy adott típus mögé írva az ilyen típusú elemekből képzett listát jelöli. Balra köt, így pl. 'a list list egy 'a típusú elemekből álló listák listáját jelöli.

4. Vegyünk egy részlegesen alkalmazható függvényt, például:
   fun valami x y = x;
   
   Nyilván itt y értéke tetszőleges, nem befolyasolja a függvény eredményét. A függvény az x paraméter értékét adja vissza, a típusa: 'a -> 'b -> 'a. Mivel a -> operátor jobbra köt, ez így értelmezendő:
   'a -> ('b -> 'a)
   
   Emlékezzünk vissza, hogy minden függvény csak egy paraméterű lehet, tehát a valami függvénynek itt csak az x a paramétere. Ez a valami x egy másik függvényt fog visszaadni, amelynek az y lesz a paramétere.

   Vagyis a valami fugggény paraméterként kap egy 'a típusú értéket: ez lesz az x. Visszaad egy függvényt. Ez a visszaadott függvény paraméterként kap egy 'b típusú értéket: méghozzá az y-t. Ennek visszatérési értéke az x érték lesz, amelyről ugye már tudjuk, hogy 'a típusú.

   Hogy egy kicsit érthetőbb legyen a dolog, nézzük egy példát valami x y-ra, azaz a valami függvény ,,teljes'' alkalmazására:

   valami 3 4
   
   válaszul 3-at kapunk. Részlegesen alkalmazva a függvényt:
   valami 3
   
   válaszul egy függvényt kapunk, amelynek van 1 paramétere, de annak értékétől függetlenül 3-at ad vissza, tehát gyakorlatilag konstansfüggvény.

5. Eddig általánosságban beszéltünk, és célszerű egy feladat megoldásakor is először így általánosságban levezetni a típust. A konkrét típusokat, úgymint int, real, bool, unit stb. - ahol ezeket egyáltalán meg lehet állapítani - kétféleképpen lehet meghatározni:
   1. fun valami (a : real) = a;
      
      A : és egy típusnév segítségével előírhatjuk egy meghatározatlan típusú kifejezés típusát. Itt a típusát real-re állítottuk. Fontos a zárójelezés, mivel a ,,típuscastolás'' nagyon alacsony precedenciájú. Mindjárt meglátjuk, mi lenne zárójelek nélkül.

      A függvény típusa most: real -> real, ugyanis explicite előírtuk, hogy a paramétere real típusú legyen, és mivel a visszatérési értéke megegyezik az átadott paraméter értékével (identitásfüggvényről lévén szó), ezért nyilván az is real típusú.

      fun valami a : real = a;
      
      Itt most a real típust nem az a paraméterre, hanem a függvény eredményére írtuk elő! Az eredmény itt ettől függetlenül ugyanaz, de egyéb esetekben ez nem feltétlenül teljesül.

   2. A beépített függvények mindegyikére megvan, hogy milyen típusokat vár el és ad vissza alapértelmezésként. A legtöbb aritmetikai függvény alapértelmezésben int típusokkal dolgozik, a / viszont real-lel. Többszörösen terhelt nevek esetén az alapértelmezéseket felül lehet bírálni, ha explicite megadjuk a típusokat, mint az előző pontban láttuk.

      Másrészt meghatározó a számkonstansok típusa is. Így pl.

      • fun valami x = 2 * x esetén valami: int -> int.

      • fun valami x = 2.3 * x esetén valami: real -> real.

      • fun valami x = x/2 hibás, mivel a / operátor real operandusokat vár, a 2 viszont int típusú.

      • fun valami x = x / 2.0 esetén valami: real -> real.

      • fun valami x = x > 2 esetén valami: int -> bool.

      • fun valami x = x > 2.0 esetén valami: real -> bool.

   3. Fontos még a ''a, ''b, ''c stb. alakú típusváltozók említése is. Ezek ugyanolyanok, mint a 'a, azzal a különbséggel, hogy a '' azt jelzi: a típuson elvégezhetőnek kell lennie az egyenlőségvizsgálatnak. Pl. két int egyenlősége vizsgálható, tehát a ''a konkrétan lehet int, viszont nem lehet pl. real -> int, mert függvények egyenlőségét nem lehet megvizsgálni.
      fun valami (x,y) = x = y;
      
      A típusa: ''a * ''a -> bool. A bool visszatérési érték nyilvánvalóan az = operátorból adódik. A ''a jelöli, hogy a konkrét típusoknak egyenlőségvizsgálatot megengedő típusoknak kell lenniük. Megfigyelhető még az is, hogy mindkét paraméter ''a típusú. Ez azért van, mert ''a * ''b -> bool típus esetén pl. megpróbálhatnánk összehasonlítani egy string-et egy int-tel, aminek nyilván kevés értelme lenne!

14.16. Kérdés.

Mit tegyek, ha az sml nem enged meg olyan dolgokat, mint a Prolog, például önmagát tartalmazó listákat... Konkrétabban az alábbi Prolog-eljárást szeretném megvalósítani sml-ben:

lls(0, []) :- !.
lls(N, [L|L]):- N1 is N-1, lls(N1, L).

Ha valakinek sikerül, légyszi szóljon!

14.16. Válasz.

Oktató: Az SML szigorú típusossága miatt ez nem sikerülhet. Más utat kell keresnie.

14.17. Kérdés.

Arra lennék kíváncsi, hogy ennek mi a típusa?

val x = fn (z, y, f) => f y z

x : 'a * 'b * ('b -> 'a -> 'c) -> 'c

az mosml szerint, de ez hogyan jön ki? Mert ha nézem a jobb oldalt, akkor

z = 'a
y = 'a -> 'b
f = 'a -> 'b -> 'c

és akkor 'a * 'b * 'c-nek kellene lennie ott, nem? (Úgy láccik, hogy nem, de miért?)

14.17. Válasz.

Hallgató: Vigyázz, az y nem függvény! Így kellett volna felírnod:

y : 'a
z : 'b
f : 'a -> 'b -> 'c
x : 'b * 'a * ('a -> 'b -> 'c) -> 'c

amiből névcserével megkapod az mosml válaszát.

A kérdező folytatja: Amire még kíváncsi lennék:

val x = fn p => fn (q, r) => p q r

Hallgató: Szerintem az előzőhöz hasonló fejtegetéssel:

q : 'a
r : 'b
p : 'a -> 'b -> 'c
x : ('a -> 'b -> 'c) -> 'a * 'b -> 'c

14.18. Kérdés.

Kisegítene valaki, hogy mi az f típusa és miért:

fun f g (h,i) = g (i,h) i

14.18. Válasz.

Oktató: Annyit magyaráztuk már ezeket a típusegyenleteket! Ha még mindig nem érti, olvassa el a <http://dp.iit.bme.hu/sml/eloadas_anyagok/fpTiplev/tipuslevezetes.html> <http://dp.iit.bme.hu/sml/eloadas_anyagok/tipuslevezetes.pdf> segédletet, abból talán megérti, hogy az mosml szerint az f típusa miért éppen ez:

('a * 'b -> 'a -> 'c) -> 'b * 'a -> 'c

14.19. Kérdés.

Jó szokásomhoz híven :) akadt megint egy-két dolog, ami nem teljesen világos. Kérem, aki tud, segítsen, mert fogy az idő...

- val v2 = app (print o str);
> val v2 = fn : char list -> unit

Szóval ez az eredmény hogyan jön ki? Elsősorban az app függvényre vagyok kíváncsi, de az egész megoldás menetét sem vetném meg. :)

14.19. Válasz.

Oktató: Nézzük az alkalmazott függvények típusát:

str   : char -> string
print : string -> unit
o     : ('a -> 'b) * ('c -> 'a) -> 'c -> 'b infix!

A behelyettesítések:

    ('c -> 'a) <-- (char -> string) és
    ('a -> 'b) <-- (string -> unit) , azaz
    'a <-- string,
    'b <-- unit,
    'c <-- char

A print o str kifejezés eredménye egy függvény, az str és a print kompozíciója. A behelyettesítések után a típusa: char -> unit. Erre a függvényre alkalmazzuk app-ot, amelynek az első paramétere van csak lekötve.

app : ('a -> unit) -> 'a list -> unit

A behelyettesítések:

    ('a -> unit) <-- (char -> unit) , azaz
    'a <-- char.

app (print o str) = v2 típusa az 'a <-- char behelyettesítéssel: char list -> unit. (A v2 egy karakterlista elemeit írja ki a standard outputra.)

A kérdező folytatja: A kérdésem ugyanaz, mint előbb...

- val v4 = map (String.fields Char.isPunct);
> val v4 = fn : string list -> string list list

Oktató: A válasz is ugyanaz: el kell végezni a behelyettesítéseket a megfelelő sorrendben!

String.fields : (char -> bool) -> string -> string list
Char.isPunct  : char -> bool
(String.fields Char.isPunct) : string -> string list
map : ('a -> 'b) -> 'a list -> 'b list

('a -> 'b) <-- (string -> string list) , tehát
'a <-- string,
'b <-- string list

Továbbá

(map f) típusa: 'a list -> 'b list

ui. első paramétere le van kötve az f : 'a -> 'b függvénnyel! Azaz

map (String.fields Char.isPunct) == v4 típusa tehát a

behelyettesítések után

string list -> string list list

A kérdező folytatja: A következő feladatban sajnos még az eredmény sincs meg, mert nem tudtam rájönni, hogyan lehetne beinklúdolni a Math struktúrát. use "Math.uo", use "Math.ui", use "Math.sig"? Egyik se volt elég jó... :)

val v5 = foldr op:: [Math.sin];

Hallgató: Nem inklúdolni, hanem lódolni kell: load "Math". Úgy emlékszem, ez még a diákon is szerepel, nemcsak az mosml manualban.

Oktató: Nem lesz meglepő, amit írok: el kell végezni a behelyettesítéseket...

op::       : 'a * 'a list -> 'a list
[Math.sin] : (real -> real) list
foldr      : ('A * 'B -> 'B) -> 'B -> 'A list -> 'B

Kisbetűk helyett nagybetűket használtam, hogy különbözzenek op:: típusváltozóitól.

('A * 'B -> 'B) <-- 'a * 'a list -> 'a list,
'B <-- (real -> real) list , azaz
'A <-- 'a,
'B <-- 'a list == (real -> real) list,
'A == 'a <-- (real -> real)

foldr op:: [Math.sin] == v4

típusa (a foldr első két argumentuma van lekötve):

v4: 'A list -> 'B , és a behelyettesítés után
(real -> real) list -> (real -> real) list