Skip to content

Instantly share code, notes, and snippets.

@max630 max630/Foo.hs
Last active Jan 10, 2016

Embed
What would you like to do?
attempt to use DataKinds
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE ExplicitNamespaces #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Foo where
import Prelude hiding ((-))
import GHC.TypeLits (Nat, type (-), type (<=))
import Data.Proxy (Proxy(Proxy))
class Foo (n :: Nat) x y | n x -> y, x y -> n where
foo :: Proxy n -> x -> y
instance Foo 0 (x,a) x where
foo _ (x,_) = x
reduce :: Proxy n -> Proxy (n - 1)
reduce _ = Proxy
instance (Foo (n - 1) x y, 1 <= n) => Foo n (a,x) y where
foo n (_,x) = foo (reduce n) x
-- > :l Foo
-- *Foo> :set -XDataKinds
-- *Foo> foo (Proxy :: Proxy 0) ("",(2::Int,True))
-- ""
-- *Foo> foo (Proxy :: Proxy 1) ("",(2::Int,True))
-- 2
-- *Foo> foo Proxy ("",(2::Int,True)) :: String
-- ""
-- *Foo> foo Proxy ("",(2::Int,True)) :: Int
-- 2
-- *Foo> foo Proxy ("",(2::Int,("a",()))) :: String
-- ""
-- *Foo> foo (Proxy :: Proxy 2) ("",(2::Int,("a",()))) :: String
-- "a"
@max630

This comment has been minimized.

Copy link
Owner Author

commented Jan 10, 2016

But:

*Foo> foo Proxy ((1,(2,3)) :: (Int,(Int,Int))) :: Int

<interactive>:28:1:
    Couldn't match type ‘1 GHC.TypeLits.<=? n0’ with ‘'True’
    The type variable ‘n0’ is ambiguous
    In the expression:
        foo Proxy ((1, (2, 3)) :: (Int, (Int, Int))) :: Int
    In an equation for ‘it’:
        it = foo Proxy ((1, (2, 3)) :: (Int, (Int, Int))) :: Int

PS: version 2 suddenly works

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.