Tip-indeksli GADTs

Question

forall hakkında kafam karıştı 'tür' GHC 8.0.1'de tür-tür imzaları türüne karşı farklı tür kontrolleri üreten türlere tanıtılan (?) GADT'lerle garip bir durumla karşılaştım davranışlar.

aşağıdaki veri türlerini göz önünde bulundurun:

{-# LANGUAGE TypeInType, GADTs, ExplicitForAll #-} 
-- Same thing happens when we replace ExplicitForAll with ScopedTypeVariables 

import Data.Kind 

data F (k :: * -> *) where 

data G :: F k -> * where 
    G :: G x 

Bu veri tipi gayet güzel derler. Ancak, G yapıcıda x türünü belirtmek istiyorsak, bir tür hatası alırız. Biz (veya oluşturucu içinde forall olmadan) tür imzaya forall eklerseniz

data H :: F k -> * where 
    H :: forall k' (x :: F k'). H x 

hata mesajı, hiçbir hata var

• Kind variable ‘k’ is implicitly bound in datatype 
    ‘H’, but does not appear as the kind of any 
    of its type variables. Perhaps you meant 
    to bind it (with TypeInType) explicitly somewhere? 
• In the data declaration for ‘H’ 

olduğunu.

data I :: forall k. F k -> * where 
    I :: I x 

data J :: forall k. F k -> * where 
    J :: forall k' (x :: F k'). J x 

Neler oluyor?

Answer 1

TypeInType Yazar. K. A. Buhr hemen yukarıda alır; Bu sadece bir böcek. HEAD'de sabitlendi. aşırı meraklı İçin

: Bu hata mesajı

data Proxy (a :: k) = Proxy 

Data.Proxy alınabilir nerede

data J = forall (a :: k). MkJ (Proxy a) 

gibi tanımları ortadan kaldırmak için tasarlanmıştır. Haskell98 stili sözdiziminde bir veri türü bildirirken, varolan niceliklendirilmiş değişkenler, forall ile açıkça kapsam içine alınmalıdır. Ancak k hiçbir zaman kapsamı açık bir şekilde getirilmemiştir; Sadece a türünde kullanılır. Yani bu, k'un evrensel olarak sayısallaştırılması gerektiği anlamına gelir (başka bir deyişle, J'a parametresi gibi için görünmez bir parametre olmalıdır) ... ancak J yazarken, ne olmalıdır, ne k'un ne olması gerektiğini belirlemenin hiçbir yolu yoktur bu yüzden her zaman belirsiz olurdu. (Buna karşılık, biz a 'ın tür bakarak Proxy için k parametre için seçim keşfedebilir.)

J için Bu tanım 8.0.1 ve HEAD izin verilmemiş olsa.