Создайте переменную типа в Haskell - PullRequest
Новая
       49

Создайте переменную типа в Haskell

5 голосов
/ 21 декабря 2010

РЕДАКТИРОВАТЬ: Решено. Я не знал, что включение расширения языка в исходном файле не включало расширение языка в GHCi. Решение было :set FlexibleContexts в GHCi.

Недавно я обнаружил, что объявления типов в классах и экземплярах в Haskell являются предложениями Horn. Поэтому я закодировал арифметические операции из Искусство Пролога , Глава 3, в Хаскелл. Например: 

fac(0,s(0)).
fac(s(N),F) :- fac(N,X), mult(s(N),X,F).

class Fac x y | x -> y
instance Fac Z (S Z)
instance (Fac n x, Mult (S n) x f) => Fac (S n) f

pow(s(X),0,0) :- nat(X).
pow(0,s(X),s(0)) :- nat(X).
pow(s(N),X,Y) :- pow(N,X,Z), mult(Z,X,Y).

class Pow x y z | x y -> z
instance (N n) => Pow (S n) Z Z
instance (N n) => Pow Z (S n) (S Z)
instance (Pow n x z, Mult z x y) => Pow (S n) x y

В Прологе значения создаются для (логической) переменной в доказательстве. Тем не менее, я не понимаю, как создавать экземпляры переменных типов в Haskell. То есть я не понимаю, что такое эквивалент Хаскелла запроса Пролога 

?-f(X1,X2,...,Xn)

есть. Я предполагаю, что 

:t undefined :: (f x1 x2 ... xn) => xi

приведет к тому, что Haskell создаст экземпляр xi, но это дает ошибку Non type-variable argument in the constraint, даже если FlexibleContexts включено.

1 Ответ

3 голосов
/ 21 декабря 2010

Не уверен насчет образцов Пролога, но я бы определил это в Haskell следующим образом: 

{-# LANGUAGE MultiParamTypeClasses, EmptyDataDecls, FlexibleInstances,
FlexibleContexts, UndecidableInstances, TypeFamilies, ScopedTypeVariables #-}

data Z
data S a
type One = S Z
type Two = S One
type Three = S Two
type Four = S Three 


class Plus x y r
instance (r ~ a) => Plus Z a r
instance (Plus a b p, r ~ S p) => Plus (S a) b r

p1 = undefined :: (Plus Two Three r) => r


class Mult x y r
instance (r ~ Z) => Mult Z a r
instance (Mult a b m, Plus m b r) => Mult (S a) b r

m1 = undefined :: (Mult Two Four r) => r


class Fac x r
instance (r ~ One) => Fac Z r
instance (Fac n r1, Mult (S n) r1 r) => Fac (S n) r

f1 = undefined :: (Fac Three r) => r


class Pow x y r
instance (r ~ One) => Pow x Z r
instance (r ~ Z) => Pow Z y r
instance (Pow x y z, Mult z x r) => Pow x (S y) r

pw1 = undefined :: (Pow Two Four r) => r

-- Handy output
class (Num n) => ToNum a n where
    toNum :: a -> n
instance (Num n) => ToNum Z n where
    toNum _ = 0
instance (ToNum a n) => ToNum (S a) n where
    toNum _ = 1 + toNum (undefined :: a) 

main = print $ (toNum p1, toNum m1, toNum f1, toNum pw1)

Обновление:

Как отметил Данпортин в своем комментарииниже TypeFamilies «Ленивый шаблон» (в контексте контекста) здесь не нужен (его исходный код короче и намного чище).

Одно применение этого шаблона, которое я могу придумать в контексте этого вопросаэто: скажем, мы хотим добавить булеву логику в нашу арифметику на уровне типов: 

data HTrue
data HFalse

-- Will not compile
class And x y r | x y -> r
instance And HTrue HTrue HTrue
instance And a b HFalse -- we do not what to enumerate all the combination here - they all HFalse

Но это не скомпилируется из-за «конфликта функциональных зависимостей».И мне кажется, что мы все еще можем выразить этот перекрывающийся случай без fundeps: 

class And x y r
instance (r ~ HTrue) => And HTrue HTrue r
instance (r ~ HFalse) => And a b r

b1 = undefined :: And HTrue HTrue r => r   -- HTrue
b2 = undefined :: And HTrue HFalse r => r  -- HFalse

Это определенно не самый хороший способ (он требует IncoherentInstances).Поэтому, возможно, кто-то может предложить другой, менее «травмирующий» подход.

...