[Haskell-ELTE] Funkcionalis fuggosegek

[Peter Divianszky]

Alakítottam még rajta kicsit...

-------------------------------------------
{-# LANGUAGE TypeOperators, TypeFamilies, UndecidableInstances #-}

data Zero   = Z
data Succ n = S n

type a :%: b = X Zero a b

type family X a b c

type instance X Zero     b        Zero     = b
type instance X Zero     Zero     (Succ a) = Zero
type instance X Zero     (Succ b) (Succ a) = X a b (Succ a)
type instance X (Succ x) Zero     (Succ a) = X x a Zero
type instance X (Succ x) (Succ b) a        = X x b a

--------- tests

n1 = S Z
n2 = S n1
n3 = S n2
n4 = S n3
n5 = S n4
n6 = S n5

(%) :: a -> b -> a :%: b
(%) = undefined

test :: (Zero, Zero, Zero, Zero, Zero, Zero)
test = (n2 % n2, n6 % n2, n6 % n3, n6 % n1, Z % n3, Z % Z)

test' :: (Succ Zero, Succ (Succ Zero), Succ (Succ Zero))
test' = (n3 % n2, n2 % Z, n5 % n3)

-------------------------------------------



2010-05-13 21:51 keltezéssel, Peter Divianszky írta:
> Sziasztok!
>
> Szerintem a következő a hiba a kódban:
>
>  > instance (...) => Divides (Succ q) (Succ p) False
>  > instance (...) => Divides (Succ q) (Succ p) b
>
> Ilyen úgy tűnik nem szabad csinálni, még akkor sem ha a (...) részen
> egymást kizáró esetek vannak.
> Viszont egy kis trükközéssel megoldható.
> Kell definiálni egy segéd Divides' osztályt, aminek eggyel több
> paramétere van, ahol megkapja azt hogy a két szám hogy viszonyul
> egymáshoz. Nem akarom hosszan magyarázni, inkább elküldöm a kódot.
> Funkcionális függőségek helyett típusfüggvényeket használok mert azokat
> részesítem előnyben, de ugyanez a trükk használható funkc. függőségekkel
> is (én is lestem másoktól...).
>
> Üdv,
> Péter
>
> 2010-05-08 12:20 keltezéssel, Dr. ERDI Gergo írta:
>> Hi,
>>
>> Adott az alabbi ket tipusosztaly es peldanyaik:
>>
>> class Lt x y b | x y -> b where
>> _lt :: x -> y -> b
>> instance Lt Zero (Succ n) True
>> instance Lt n Zero False
>> instance (Lt x y b) => Lt (Succ x) (Succ y) b
>>
>>
>> class Divides q p b | q p -> b where
>> _divides :: q -> p -> b
>> instance Divides (Succ q) Zero True
>> instance (Lt (Succ p) (Succ q) True) => Divides (Succ q) (Succ p) False
>> instance (Lt q (Succ p) True, Sub (Succ p) (Succ q) p', Divides (Succ q)
>> p' b) => Divides (Succ q) (Succ p) b
>>
>> es adott az alabbi modon definialt "2":
>>
>> type N2 = Succ (Succ Zero)
>> n2 = undefined :: N2
>>
>> Kerdesem, hogy mit jelent az alabbi hibauzenet, ha a _divides n2 n2
>> tipusat akarom meghataroztatni a GHC-vel:
>>
>> *Main> :t _divides n2 n2
>>
>> Top level:
>> Couldn't match expected type `True' against inferred type `False'
>> When using functional dependencies to combine
>> Lt n Zero False,
>> arising from the dependency `x y -> b'
>> in the instance declaration at TypeProg.hs:63:9
>> Lt Zero Zero True,
>> arising from a use of `_divides' at <interactive>:1:0-13
>>
>> ?
>>
>> Kosz,
>> Cactus