Экземпляры Eq или Ord для экзистенциального GADT
Вот что происходит с входным буфером при запуске вашей программы:
std::cin >> name;
Вы ждете ввода. Когда вы вводите «Ryan Cleary» и нажимаете enter, входной буфер содержит:
Ryan Cleary\n
Теперь ваш cin читает ввод как обычно, останавливаясь в пробеле, оставляя ваш буфер следующим образом:
Cleary\n
Обратите внимание на начальное пространство, так как оно останавливается после прочтения Ryan. Ваша первая переменная теперь содержит Ryan. Если, однако, вы хотите получить полное имя, используйте std::getline . Он будет читать до новой строки, а не только пробелов. В любом случае, продолжайте:
std::cin >> age;
Теперь вы получаете еще один вход. Тем не менее, там что-то есть. Он пропускает пробел, пока он не начнет чтение, оставив буфер только:
\n
Ваша вторая переменная получает текст Cleary. Обратите внимание на новую строку в буфере, которая возвращает меня ко второй части. Замена system ("pause"); таким образом, который всегда работает, является сложной задачей. Лучше всего жить с решением, отличным от совершенства, или, как мне нравится, тем, что не гарантируется, что он точно говорит:
std::cin.get(); //this consumes the left over newline and exits without waiting
Хорошо, поэтому cin.get() не работает. Как насчет этого:
std::cin.get(); //consume left over newline
std::cin.get(); //wait
Это работает отлично, но что, если вы скопируете-вставьте его где-нибудь, где новая строка не останется? Вам нужно нажать дважды!
Решение состоит в том, чтобы очистить новую строку (и все остальное), а затем подождать. Это цель cin.sync() . Однако, как видно из раздела примечаний, не гарантируется очистка буфера, как он говорит, поэтому, если ваш компилятор не захочет, его нельзя использовать. Для меня, тем не менее, он делает именно это, оставляя решение:
std::cin.sync(); //clear buffer
std::cin.get(); //wait
. Самое главное в system("pause"); заключается в том, что вы не знаете, какую программу он будет запускать на чужом компьютере. Они могли бы изменить pause.exe или перенести тот, который был найден первым, и вы не знаете. Это может потенциально разрушить их компьютер из-за того, что это возможно любая программа .
1 ответ
Начиная с вашего примера
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE DataKinds, KindSignatures #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
import Data.Type.Equality
data Car
data Food
data CarRental = CarRental {passengers :: Int, mileage :: Int}
deriving (Eq, Ord)
data ErrandList = ErrandList {avoidJunkFood :: Bool}
deriving (Eq, Ord)
data GetStuff a where
RentACar :: CarRental -> GetStuff Car
BuyFood :: ErrandList -> GetStuff Food
data Some t = forall a. Some (t a)
Вам нужно будет написать экземпляр http://hackage.haskell.org/package/dependent-sum-0.4/docs/Data- GADT-Compare.html # t: GEq
class GEq f where
geq :: f a -> f b -> Maybe (a :~: b)
Тогда вы сможете определить экземпляр Eq (Some f)
instance GEq f => Eq (Some f) where
Some fa == Some fb = case geq fa fb of
Just Refl -> True
Nothing -> False
Запись экземпляра вручную повторяющийся, но не ужасный. Обратите внимание, что я написал в пути без «поймать все» в последнем случае.
instance GEq GetStuff where
geq (RentACar x) z = case z of
RentACar x' -> if x == x' then Just Refl else Nothing
_ -> Nothing
geq (BuyFood x) z = case z of
BuyFood x' -> if x == x' then Just Refl else Nothing
_ -> Nothing
Существует класс GCompare для Ord ГАДЦ.
Таким образом, проблема сводится к «как получить GEq или GCompare автоматически». Я думаю, что для специальных GADT, таких как ваш GetStuff, вы можете написать quick-n-dirty TH, чтобы сгенерировать код.
Generic -подобная альтернатива, о которой я могу подумать, потребует от вас написания функций преобразования из и в GetStuff, что может быть выигрышным, если вам нужно написать более общие функции. Давайте также исследуем это. Сначала мы определим общее представление GADT, которые нас интересуют:
data Sum (cs :: [(*, *)]) a where
Z :: a :~: c -> b -> Sum ( '(c, b) ': cs) a
S :: Sum cs a -> Sum (c ': cs) a
Мы можем конвертировать между GetStuff и Sum. То, что нам нужно написать для каждого GADT, это O (n) , где n - количество конструкторов.
type GetStuffCode =
'[ '(Car, CarRental)
, '(Food, ErrandList)
]
toSum :: GetStuff a -> Sum GetStuffCode a
toSum (RentACar x) = Z Refl x
toSum (BuyFood x) = S (Z Refl x)
fromSum :: Sum GetStuffCode a -> GetStuff a
fromSum (Z Refl x) = RentACar x
fromSum (S (Z Refl x)) = BuyFood x
fromSum (S (S x)) = case x of {} -- silly GHC requires this :)
Теперь, когда у нас есть общее представление, Sum, мы можем написать общие функции. Равенство, GGEq для Родовое равенство Гадта Класс выглядит как GEq, но мы используем Sum в качестве аргументов.
class GGEq code where
ggeq :: Sum code a -> Sum code b -> Maybe (a :~: b)
Нам понадобятся два экземпляра для кодов nil и cons :
instance GGEq '[] where
ggeq x _ = case x of {}
instance (Eq b, '(x, b) ~ c, GGEq cs) => GGEq (c ': cs) where
ggeq (Z Refl x) (Z Refl y) = if x == y then Just Refl else Nothing
ggeq (S x) (S y) = ggeq x y
ggeq (Z _ _) (S _) = Nothing
ggeq (S _) (Z _ _) = Nothing
Используя этот механизм, написание geq для GetStuff тривиально: [ 1140]
geq1 :: GetStuff a -> GetStuff b -> Maybe (a :~: b)
geq1 x y = ggeq (toSum x) (toSum y)