如何在 Haskell 中编写一个简单的依赖类型函数？

Question

我正在尝试编写一个函数，其返回类型取决于其输入之一的值。

在 Idris 中，这很简单：

module Dependent

IntOrChar : Bool -> Type
IntOrChar True = Int
IntOrChar False = Char

fun : (x : Bool) -> IntOrChar x
fun True = 10
fun False = 'a'

有了这些定义：

λΠ> fun True
10 : Int
λΠ> fun False
'a' : Char

我的问题是：我可以在 Haskell 中以简单的方式做类似的事情吗？

我想我可以使用singletons 之类的东西，但我不知道如何正确使用它们。

这行得通：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}

module Main where

import Data.Singletons.Prelude

type family IntOrChar (x :: Bool) where
  IntOrChar True = Int
  IntOrChar False = Char

fun :: SBool b -> IntOrChar b
fun b = case b of
          STrue -> 10
          SFalse -> 'a'

...

λ fun STrue
10
λ fun SFalse
'a'

但这需要我使用SBools 而不是普通的Bools。我宁愿把它用作fun True。

有没有办法在 Haskell 中制作相当于 fun : (x : Bool) -> IntOrChar x 的方法？

Answer 1

我打算通过提出一个更复杂的依赖类型函数（如 Idris 中的 jammed door 示例）以及如何在 Haskell 中执行此操作来扩充我的问题。

但我找到了答案here。这是使用它的 Jammed Door 示例，供参考。

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE RankNTypes #-}

module Door where

import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Promotion.TH

$(singletons [d|
 data DoorState = DoorOpen | DoorClosed
 data DoorResult = Jammed | OK
 |])

$(promote [d|
 tryOpen :: DoorResult -> DoorState
 tryOpen Jammed = DoorClosed
 tryOpen OK = DoorOpen
 |])

data DoorCmd (res :: k) (s :: DoorState) (f :: k ~> DoorState) where
  Open :: forall check. DoorCmd check DoorClosed TryOpenSym0
  Close :: DoorCmd '() DoorOpen (ConstSym1 'DoorClosed)
  Knock :: DoorCmd '() state (ConstSym1 state)
  Pure :: forall (res :: k) (state_fn :: k ~> DoorState). Sing res -> DoorCmd res (state_fn @@ res) state_fn
  (:>>=) :: forall (a :: k1) (b :: k2) (state1 :: DoorState) (state2_fn :: k1 ~> DoorState) (state3_fn :: k2 ~> DoorState).
    DoorCmd a state1 state2_fn ->
    (Sing a -> DoorCmd b (state2_fn @@ a) state3_fn) ->
    DoorCmd b state1 state3_fn

doorOps :: DoorCmd '() DoorClosed (ConstSym1 'DoorClosed)
doorOps = do
  Knock
  result <- Open
  case result of
    SJammed -> Knock
    SOK -> Close
  where
    (>>=) = (:>>=)
    (>>) a k = a :>>= \_ -> k
    return = Pure