How to write a simple dependent type function in Haskell?

Question

I'm trying to write a function whose return type depends on the value of one of its inputs.

In Idris, it is straightforward:

module Dependent

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

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

With those definitions:

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

My question is: can I do a similar thing in a simple manner in Haskell?

I suppose I could use something like singletons, but I don't know how to use them properly.

This works:

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

But it requires me to use SBools instead of plain Bools. I'd rather use it as fun True.

Is there a way to make the equivalent of fun : (x : Bool) -> IntOrChar x in Haskell?

Singleton's how we do it since Haskell doesn't actually have dependent types. — Li-yao Xia, Jul 01 '18 at 19:03
Haskell only has GADTs, which are not as powerful as dependent types (sometimes more convenient, other times more cumbersome or just not enough). A good technical comparison between GADTs vs dependent types is in the Hasochism paper. — chi, Jul 01 '18 at 19:44
Possible duplicate of [Difference between Haskell and Idris: Reflection of Runtime/Compiletime in the type universes](https://stackoverflow.com/questions/37362342/difference-between-haskell-and-idris-reflection-of-runtime-compiletime-in-the-t) — K. A. Buhr, Jul 04 '18 at 16:39

score 0 · Answer 1 · answered Jul 09 '18 at 00:41

I was going to augment my question by proposing a more complicated dependent type function (like the jammed door example in Idris) and how to do it in Haskell.

But I found the answer here. Here is the Jammed Door example using that, for reference.

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

How to write a simple dependent type function in Haskell?

1 Answers1