Làm cách nào tôi có thể sử dụng bằng chứng mâu thuẫn?

Question

Trong khi viết about how to do subtyping in Haskell, nó xảy ra với tôi rằng nó sẽ rất thuận tiện để có thể "sử dụng" bằng chứng mâu thuẫn như True ~ False để thông báo cho trình biên dịch về các chi nhánh đã chết. Với một loại trống tiêu chuẩn, Void, phần mở rộng EmptyCase phép bạn đánh dấu một chi nhánh chết (tức là một trong có chứa một giá trị kiểu Void) theo cách này:

use :: Void -> a 
use x = case x of 

Tôi muốn làm điều gì đó tương tự cho không thể thoả mãn Constraint S.

Có thuật ngữ nào có thể được cấp loại True ~ False => a nhưng không thể được cấp loại a?

Answer 1

Bạn thường có thể làm điều này bằng cách tách bản chất chính xác của bằng chứng theo cách bạn định sử dụng. Nếu trình kiểm tra loại thấy mà bạn đã giới thiệu một ràng buộc vô lý, nó sẽ sủa vào bạn. Vì vậy, mẹo là để trì hoãn sự bình đẳng đó sau :~:, và sau đó để thao tác bằng chứng bình đẳng bằng cách sử dụng các hàm tổng hợp hợp lý.

{-# LANGUAGE GADTs, TypeOperators, ScopedTypeVariables, DataKinds, 
     PolyKinds, RankNTypes #-} 
{-# OPTIONS_GHC -Wall #-} 

module TrueFalse where 
import Data.Type.Equality 

data Foo (a :: Bool) where 
    Can :: Foo 'False 
    Can't :: (forall x . x) -> Foo 'True 

extr :: Foo 'True -> a 
extr (Can't x) = x 

subst :: a :~: b -> f a -> f b 
subst Refl x = x 

whoop :: 'False :~: 'True -> a 
whoop pf = extr $ subst pf Can 

Chức năng whoop có vẻ là khoảng những gì bạn đang tìm kiếm.

---

Như András Kovács nhận xét, thậm chí bạn có thể chỉ cần sử dụng EmptyCase trên giá trị 'False :~: 'True. Hiện tại (7.10.3), thật không may, EmptyCasedoesn't warn about non-exhaustive matches. Điều này hy vọng sẽ được sửa chữa sớm.

Answer 2

Ràng buộc như vậy sẽ gây ra lỗi loại nếu nó xuất hiện dưới dạng ràng buộc nhất định. Nói chung, điều này áp dụng cho bất kỳ ràng buộc nào mà người đánh máy xem xét là không thể.

Thậm chí viết một hàm

f :: ('True ~ 'False) => x 
f = undefined 

không typecheck, vì bối cảnh của một hàm là một hạn chế nhất định trong cơ thể của hàm - và 'True ~ 'False đơn giản là không thể xuất hiện như là một hạn chế nhất định.

Tốt nhất bạn có thể có, ví dụ:

import Data.Type.Equality ((:~:)(..)) 

type family (==) (a :: k) (b :: k) :: Bool where 
    a == a = 'True 
    a == b = 'False 

f :: ((x == y) ~ 'False) => x :~: y -> a 
-- f Refl = undefined -- Inaccessible code 
f = \case{} 

mà lại quay trở lại EmptyCase, lần này trên :~:. Lưu ý rằng

f :: ((x == y) ~ 'False, x ~ y) => a 

cũng làm giảm tới một hạn chế trivially không thể, bởi vì x == x giảm tới True. Bạn có thể viết một vị bình đẳng mà không làm giảm cho trivially loại bằng nhau (ví dụ như một trong Data.Type.Equality), cho phép bạn viết:

import Data.Type.Equality 

f :: ((x == y) ~ 'False, x ~ y) => Proxy '(x,y) -> a 
f = undefined 

Có thể có một cách để viết chức năng này mà không cần undefined nhưng nó là loại tranh luận dù sao kể từ khi loại hình này ngay lập tức được giảm GHC:

>:t f 
f :: forall (k :: BOX) (y :: k) a. ((y == y) ~ 'False) => Proxy '(y, y) -> a 

Thậm chí nếu không có sự hạn chế đó, nó là definitionally không thể gọi hàm Proxy '(y,y) -> a với hai khác nhau loại. Không có cách nào để ẩn một ràng buộc bình đẳng ~ từ máy đánh chữ - bạn phải sử dụng một hình thức bình đẳng khác, cái không giảm xuống ~.