Как написать функцию простого зависимого типа в Haskell? - PullRequest
Новая
       20

Как написать функцию простого зависимого типа в Haskell?

0 голосов
/ 01 июля 2018

Я пытаюсь написать функцию, тип возвращаемого значения которой зависит от значения одного из ее входных данных.

В Идрисе это просто: 

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?

Полагаю, я мог бы использовать что-то вроде синглетонов , но я не знаю, как правильно их использовать.

Это работает: 

{-# 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'

Но это требует, чтобы я использовал SBool с вместо простых Bool с. Я бы предпочел использовать его как fun True.

Есть ли способ сделать эквивалент в fun : (x : Bool) -> IntOrChar x в Haskell?

1 Ответ

0 голосов
/ 09 июля 2018

Я собирался дополнить свой вопрос, предложив более сложную функцию зависимого типа (например, пример заклинившей двери в Идрис ) и как это сделать в Хаскеле.

Но я нашел ответ здесь . Вот пример использования заклинившей двери для справки. 

{-# 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
...