Skip to content

Instantly share code, notes, and snippets.

@mlen

mlen/GADTs.hs

Created June 22, 2014 16:49
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save mlen/23f61025c385f8538539 to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save mlen/23f61025c385f8538539 to your computer and use it in GitHub Desktop.
Download ZIP

Revisions

  1. mlen revised this gist Jun 22, 2014. 1 changed file with 3 additions and 0 deletions.
    3 changes: 3 additions & 0 deletions gistfile1.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -1,3 +1,6 @@
    [1 of 1] Compiling Main ( GADTs.hs, interpreted )

    GADTs.hs:15:22:
    Could not deduce (b1 ~ b)
    from the context ((1 + b) ~ (1 + b1))
    bound by a pattern with constructor
  2. mlen created this gist Jun 22, 2014.
    21 changes: 21 additions & 0 deletions GADTs.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,21 @@
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE StandaloneDeriving #-}
    {-# LANGUAGE TypeOperators #-}
    import GHC.TypeLits

    data Stack :: * -> Nat -> * where
    Nil :: Stack t 0
    Cons :: a -> Stack a b -> Stack a (1 + b)

    deriving instance Show a => Show (Stack a b)

    pop :: Stack a (1 + b) -> (a, Stack a b)
    pop (Cons a b) = (a, b)

    push :: a -> Stack a b -> Stack a (1 + b)
    push = Cons

    empty :: Stack t 0
    empty = Nil
    21 changes: 21 additions & 0 deletions gistfile1.txt
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,21 @@
    Could not deduce (b1 ~ b)
    from the context ((1 + b) ~ (1 + b1))
    bound by a pattern with constructor
    Cons :: forall a (b :: Nat). a -> Stack a b -> Stack a (1 + b),
    in an equation for ‘pop’
    at GADTs.hs:15:6-13
    ‘b1’ is a rigid type variable bound by
    a pattern with constructor
    Cons :: forall a (b :: Nat). a -> Stack a b -> Stack a (1 + b),
    in an equation for ‘pop’
    at GADTs.hs:15:6
    ‘b’ is a rigid type variable bound by
    the type signature for pop :: Stack a (1 + b) -> (a, Stack a b)
    at GADTs.hs:14:8
    Expected type: Stack a b
    Actual type: Stack a b1
    Relevant bindings include
    b :: Stack a b1 (bound at GADTs.hs:15:13)
    pop :: Stack a (1 + b) -> (a, Stack a b) (bound at GADTs.hs:15:1)
    In the expression: b
    In the expression: (a, b)