[Haskell-ELTE] Funkcionalis fuggosegek

[Dr. ERDI Gergo]

Szia!

Eloszor is koszi a valaszt.
Masreszt viszont azert nem akarok tipusfuggvenyeket hasznalni, mert a GHCi 
nem normalizalva irja ki a tipusokat, es ezert a valodi eredmenyt igazabol 
nem kapom meg...
Pl. vegyuk a kovetkezo egyszeru peldat:

> {-# LANGUAGE EmptyDataDecls, TypeFamilies #-}
>
> data Zero
> data Succ n
>
> n0 = undefined :: Zero
> n1 = undefined :: (Succ Zero)
> n2 = undefined :: (Succ (Succ Zero))
> n3 = undefined :: (Succ (Succ (Succ Zero)))
>
> type family Add n m
> type instance Add n Zero = n
> type instance Add n (Succ m) = Succ (Add n m)
>
> _add :: n -> m -> Add n m
> _add = undefined

Marmost ha a GHCi-vel kiiratom az _add n2 n3 tipusat, akkor a kovetkezot 
kapom:
_add n2 n3 :: Add (Succ (Succ Zero)) (Succ (Succ (Succ Zero)))

Ami a kerdes totalis megkerulese:), hiszen pontosan tudom, hogy ketto meg 
harom osszege az ketto meg harom osszege...

Az altalanos modszert (hogy t.i. egy kulon tanuval kiegeszitem a 
tipusosztalyok parametereit) nem sikerult atvennem, viszont ezzel az X 
seged"fuggvennyel" mar  megoldottam:


> class Eq x y b | x y -> b where
>     _eq :: x -> y -> b
> instance Eq Zero Zero True
> instance (Eq x y b) => Eq (Succ x) (Succ y) b
> instance Eq Zero (Succ y) False
> instance Eq (Succ x) Zero False
>
> class X x a b d | x b a -> d
> instance                      X Zero     b        Zero      b
> instance                      X Zero     Zero     (Succ a)  Zero
> instance (X a b (Succ a) d) => X Zero     (Succ b) (Succ a)  d
> instance (X x a Zero d) =>     X (Succ x) Zero     (Succ a)  d
> instance (X x b a d) =>        X (Succ x) (Succ b) a         d
>
> class Mod p q r | p q -> r where
>     _mod :: p -> q -> r
> instance (X Zero p q r) => Mod p q r
>
> class Divides q p b | q p -> b where
>    _divides :: q -> p -> b
> instance (Mod p q r, Eq r Zero b) => Divides q p b

Ugyhogy koszi, megprobalok tovabb haladni :)

-- 

   .--= ULLA! =-----------------.   `We are not here to give users what
    \     http://gergo.erdi.hu   \   they want'  -- RMS, at GUADEC 2001
     `---= gergo at erdi.hu =-------'
Az "ígéret" szép szó, de a "dnyepropetrovszk" még szebb.