我可以使用升級類型進行分支控制嗎？

Question

我創建了一個玩具程序試圖做一個提升的類型分支：

{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, ScopedTypeVariables, GADTs #-} 
module Foo where 

import Data.Proxy 

data Out = ToInt | ToBool 

type family F (a :: Out) where 
    F ToInt = Int 
    F ToBool = Bool 

foo :: forall k. Proxy (k :: Out) -> Int -> F k 
foo p = case p of 
    (Proxy :: Proxy 'ToInt) -> id 
    (Proxy :: Proxy 'ToBool) -> (== 0) 

在這裏，我想對分支和Proxy對他們的使用顯式類型的簽名，但這不起作用，GHC抱怨：

[1 of 1] Compiling Foo    (Foo.hs, Foo.o) 

Foo.hs:15:6: error: 
    • Couldn't match type ‘k’ with ‘'ToBool’ 
     ‘k’ is a rigid type variable bound by 
     the type signature for: 
      foo :: forall (k :: Out). Proxy k -> Int -> F k 
     at Foo.hs:12:15 
     Expected type: Proxy 'ToBool 
     Actual type: Proxy k 
    • When checking that the pattern signature: Proxy 'ToBool 
     fits the type of its context: Proxy k 
     In the pattern: Proxy :: Proxy ToBool 
     In a case alternative: (Proxy :: Proxy ToBool) -> (== 0) 
    • Relevant bindings include 
     p :: Proxy k (bound at Foo.hs:13:5) 
     foo :: Proxy k -> Int -> F k (bound at Foo.hs:13:1) 

我認爲這基本上說GHC有困難搞清楚第二個分支k ~ 'ToBool。 （實際上第一個分支不工作或者爲非常類似的錯誤信息）

這是真的可能或我做錯了什麼？

Answer 1

這是不可能的。類型被刪除，所以你不能直接使用它們在運行時做出決定。通常的做法是用一個單例替換代理。在這種情況下，我認爲類型家庭是過度殺傷性的，所以我放棄了它。

data Out a where 
    ToInt :: Out Int 
    ToBool :: Out Bool 

foo :: forall k. Out k -> Int -> k 
foo p = case p of 
    ToInt -> id 
    ToBool -> (== 0) 

如果你願意，你可以改用DataKinds促進您Out構造函數和指數單類型那些：

data OutS a where 
    ToIntS :: OutS 'ToInt 
    ToBoolS :: OutS 'ToBool 

foo :: forall k. OutS k -> Int -> F k 
foo p = case p of 
    ToIntS -> id 
    ToBoolS -> (== 0) 

但在這種情況下，我不知道有多大的點。

另一個設計選項（它可以用任何一種上述用途）是使用一個類，以配合一型到其單：

class SConv t where 
    sConv :: proxy t -> OutS t 
instance SConv 'ToInt where 
    sConv _ = ToIntS 
instance SConv 'ToBool where 
    sConv _ = ToBoolS 

這使得單傳遞一個比特多個隱式的情況。

希望理查德艾森伯格能在未來幾年內完成他的DependentHaskell工作，在這一點上，這一切都將變得不那麼痛苦。