代码之家 › 专栏 › 技术社区 › nicolas

签名中的绑定类型

type-level-computation haskell

2

nicolas · 技术社区 · 7 年前

当GATT中的模式匹配时,绑定类型变量最直接的方法是什么?

#!/usr/bin/env stack
-- stack script --resolver lts-13.1
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs, ScopedTypeVariables             #-}
{-# LANGUAGE DataKinds   #-}
module Main where
import Data.Proxy
import GHC.TypeLits    
main :: IO ()
main = undefined

data Kind where
  Index :: Symbol -> Kind

data Gadt (f::Kind) where
  Lit :: KnownSymbol s => Gadt ('Index s)

结合 s 直接失败

format :: Gadt f -> String
format (Lit :: Gadt ('Index s)) = undefined   -- KO

有误差

â¢ Couldn't match type âfâ with â'Index sâ
  âfâ is a rigid type variable bound by
    the type signature for:
      format :: forall (f :: Kind). Gadt f -> String
  Expected type: Gadt f
  Actual type: Gadt ('Index s)

类型函数可以提取类型,但是否没有更直接的方法来实现这一点?

format (Lit :: Gadt i)  =  symbolVal (Proxy :: TLabel i)

type family TLabel (a::Kind)
type instance TLabel ('Index s  ) = Proxy s

1 回复 | 直到 7 年前

1

3

Li-yao Xia 7 年前

我看到的唯一方法是添加 Proxy 将类型变量与 ScopedTypeVariables .

data Gadt a where
  Lit :: KnownNat s => Proxy s -> Gadt ('Index s)

format :: Gadt a -> String
format (Lit (Proxy :: Proxy s)) = undefined

如果您担心额外的分配,可以将字段解包。(编辑:删除以前提到的 Proxy# 因为这似乎不必要)。

import Data.Proxy

-- This should be as efficient as the original Gadt with a nullary Lit
data Gadt a where
  Lit :: {-# UNPACK #-} !(Proxy r) -> Gadt ('Index r)

format :: Gadt a -> String
format (Lit (_ :: Proxy r)) = undefined

从长远来看,以下GHC提案将解决这一问题: Type Applications in Patterns .

-- The original type
data Gadt a where
  Lit :: forall s. Gadt ('Index s)

format :: Gadt a -> String
format (Lit @s) = ...