Общая информация «typeless» STack in Haskell

Question

Мне нужно реализовать общий стек для чего-то, над чем я работаю. Этот стек должен содержать элементы разных типов. Например, (1, 'c', True, "Strings"). Поддерживаемые функции: верх, поп и толчок.

Кортежи - самая естественная идея для этого.

push x s = (x,s) 
pop s = snd s 
top s = (fst s, s) 

Но мне также нужно поддерживать пустой стек. Здесь pop и top не определены в(). Итак, я попытался создать новый тип.

data Stack = Empty | forall x. Cons (x, Stack) 
push x s = Cons (x,s) 
pop s = case s of 
     Empty -> Left s 
     Cons (x, y) -> Right y 
top s = case s of 
     Empty -> (Left(), s) 
     Cons (x,y) -> (Right x, s) 

Здесь, сверху дает мне ошибку:

Couldn't match expected type ‘b’ with actual type ‘x’ 
    because type variable ‘x’ would escape its scope 
This (rigid, skolem) type variable is bound by 
    a pattern with constructor 
    Cons :: forall x. (x, Stack) -> Stack, 
    in a case alternative 
    at try.hs:11:9-18 
Relevant bindings include 
    x :: x (bound at try.hs:11:15) 
    top :: Stack -> (Either() b, Stack) (bound at try.hs:9:1) 
In the first argument of ‘Right’, namely ‘x’ 
In the expression: Right x 

Если я работаю вокруг этого с:

data Stack x = Empty | forall y. Cons (x, Stack y) 

я получаю ту же ошибку для поп-музыки.

Я также попытался добавить это:

type AnyStack = forall x. Stack x 

но опять-таки получить подобную ошибку:

Couldn't match expected type ‘b’ with actual type ‘Stack y’ 
    because type variable ‘y’ would escape its scope 
This (rigid, skolem) type variable is bound by 
    a pattern with constructor 
    Cons :: forall x y. (x, Stack y) -> Stack x, 
    in a case alternative 
    at try.hs:8:9-19 
Relevant bindings include 
    y :: Stack y (bound at try.hs:8:18) 
    pop :: Stack t -> Either (Stack t) b (bound at try.hs:6:1) 
In the first argument of ‘Right’, namely ‘y’ 
In the expression: Right y 

Может кто-нибудь помочь мне с подписями правильного типа или определения типа для такого стека ? Или, может быть, назовите меня хорошей ссылкой, связанной с этим?

Большое спасибо за продвинутый!

Edit:

Было бы идеально, если я был бы в состоянии включить функцию ПОЛУЧИТЬ для этого стека. Учитывая целое число i и стек s, get будет возвращать i-й элемент s. Я надеялся, что, возможно, я смогу сделать это сам, как только толчок, поп и верх будут отсортированы, но я все еще не могу. Любые идеи относительно этих парней?

Answer 1

Нужно ли это иметь нетипизированное?Если вы готовы использовать расширенные функции GHC, вы можете сделать что-то вроде этого:

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeOperators #-} 
{-# LANGUAGE FlexibleInstances, FlexibleContexts #-} 

module Stack (Stack(..), push, pop, top, empty) where 

data Stack (h :: [*]) where 
    Empty :: Stack '[] 
    Push :: x -> Stack xs -> Stack (x ': xs) 

instance Show (Stack '[]) where 
    showsPrec d Empty = showParen (d > 11) $ showString "Empty" 

instance (Show x, Show (Stack xs)) => Show (Stack (x ': xs)) where 
    showsPrec d (Push x xs) = showParen (d > 10) $ 
     showString "Push " . showsPrec 11 x . showChar ' ' . showsPrec 11 xs 

instance Eq (Stack '[]) where 
    _ == _ = True 

instance (Eq x, Eq (Stack xs)) => Eq (Stack (x ': xs)) where 
    (Push x xs) == (Push y ys) = x == y && xs == ys 

instance Ord (Stack '[]) where 
    compare _ _ = EQ 

instance (Ord x, Ord (Stack xs)) => Ord (Stack (x ': xs)) where 
    compare (Push x xs) (Push y ys) = case compare x y of 
    EQ -> compare xs ys 
    LT -> LT 
    GT -> GT 


push :: x -> Stack xs -> Stack (x ': xs) 
push = Push 

pop :: Stack (x ': xs) -> Stack xs 
pop (Push _ xs) = xs 

top :: Stack (x ': xs) -> x 
top (Push x _) = x 

empty :: Stack '[] 
empty = Empty 

Несколько использует в GHCI выглядеть следующим образом:

[1 of 1] Compiling Stack   (typelist.hs, interpreted) 
Ok, modules loaded: Stack. 
*Stack> :t push True . push (Just 'X') . push 5 . push "nil" $ empty 
push True . push (Just 'X') . push 5 . push "nil" $ empty 
    :: Num x => Stack '[Bool, Maybe Char, x, [Char]] 
*Stack> push True . push (Just 'X') . push 5 . push "nil" $ empty 
Push True (Push (Just 'X') (Push 5 (Push "nil" Empty))) 
*Stack> pop . push True . push (Just 'X') . push 5 . push "nil" $ empty 
Push (Just 'X') (Push 5 (Push "nil" Empty)) 
*Stack> pop empty 

<interactive>:75:5: 
    Couldn't match type ‘'[]’ with ‘x0 : xs’ 
    Expected type: Stack (x0 : xs) 
     Actual type: Stack '[] 
    Relevant bindings include 
     it :: Stack xs (bound at <interactive>:75:1) 
    In the first argument of ‘pop’, namely ‘empty’ 
    In the expression: pop empty 

Обратите внимание, что это представление имеет хорошую особенность, что это ошибка времени компиляции для вызова pop или top на пустой стек. С этим немного сложнее работать, поскольку вам всегда нужно доказать, что вы вызываете его с непустым стеком. Это полезно для предотвращения ошибок, но иногда требуется больше бухгалтерского учета, чтобы убедить компилятор, что у вас все получилось. Неверно, что это представление - хороший выбор. Это зависит от варианта использования.

Answer 2

Вы не сможете определить поп в пустом кортеже, но остальное достаточно гладко, если мы используем класс типа для представления случаев в типе стека.

class Stack h where 
    push :: a -> h x -> h (a, x) 
    pop :: h (a, x) -> (h x, a) 
    top :: h (a, x) -> (h (a, x), a) 
    top hax = let (_, a) = pop hax in (hax, a) 

newtype S x = S x 

instance Stack S where 
    push a (S x) = S (a, x) 
    pop (S (a, x)) = (S x, a) 

Если вы подвергаете пуш/поп/верх и S отвлеченно вместе с

sempty :: S() 
sempty = S() 

Вы можете убедиться, что никто не может строить патологические стеки. Если у вас все в порядке с GADT, тогда есть более удобные кодировки.

data S h where 
    Nil :: S() 
    Cons :: a -> S x -> S (a, x) 

Вы можете открыть этот GADT напрямую, поскольку он уже не может иметь нарушения типа.

instance Stack S where 
    push = Cons 
    pop (Cons a x) = (x, a)